[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: categories: Reality check
> > [Discussion about intuitionistic versions of Freyd's construction
> > deleted.]
So, in response to that aspect:
Peter's motivation was to capture the signed binary interval rather
than the binary one, a distinction that only exists in an
intuitionistic setting. For (at least) this reason, his original
definition was already intuitionistic (indeed his axioms were
explicitly formulated in an intuitionistically appropriate form).
The point I was making was that, given that one is already being
sensitive to intuitionistic formulations, one also needs to be
equally careful about other aspects of the axiomatization (e.g.
the definition of a suitable category of ordered sets). I was
curious to know which of the (apparently many) possible alternative
definitions Peter had in mind.
It seems to me eminently plausible that Peter's construction works
perfectly for the previously discussed intuitionistic linear orderings
(I agree with Andrej about terminology - I took my terminology
"pseudo ordering" from Peter Aczel). In fact, I would expect it to give
the closed interval of Dedekind reals in any elementary topos with nno.
(Peter's proof that one obtains the signed-binary = Cauchy interval does
indeed appear to use number-number choice.) I think that would be
a very nice result.
Peter, is this the sort of thing you're aiming at?
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113
FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209