Martin writes:
[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 -- 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 URL: http://www.dcs.ed.ac.uk/home/als