Hi Bas,

thank you - indeed this is a very interesting observation. This was the proof I had in mind when I first claimed that the axiom of choice is provable in OTT. However, I was deluded in believing that OTT/ predicative topoi exactly characterize the theory of the setoid model. As you clearly point out this is not the case. To me this is an incompleteness of the formal system (OTT/predicative topoi) wrt the intended interpretation. This should be fixable, leading to OTT+X or predicative topoi + X which should be complete wrt the setoid model. More categorically we could say that X characterizes thepredicative topoi obtained by an exact completion of an LCCC - Ithink.First of all, I am not sure whether a "fix" is needed. My recentexperience inconstructive mathematics is that it is actually quite pleasant to workwithout countable choice. Initial experience shows that it may leadto betteralgorithms implicit in the proofs. (Most of this is in my work withThierryCoquand.) As you know, choice breaks abstract datatypes. See forinstance theencoding of ADT as existential types by Mitchell and Plotkin. Thisis notpossible in dependent type theory precisely because we have choice(this waspointed out to me by Jesper Carlstrom some time ago). I understand onemotivation for your work on OTT as an attempt to bring back (some?)ADTs intype theory. It would be a pity to throw them out again without a good reason.

`I'd like to understand this better - in the moment I am unconvinced.`

`Instead of "choice", I'd like`

f : Pi a:A.(B a)/(~ a) ------------------------- lift f: (Pi a:A.B a)/~'

`for "discrete" types A, which means that I work in the internal`

`language of the setoid model. Quotient types, even with lift, seem to`

`be a good way to capture ADTs.`

`Also if you want to reject lift, it would be good to have a model`

`construction (maybe like the setoid model) which refutes it. Other`

`things which you want may become true in this model.`

Having said that here are some quick remarks on your proposal below.Having choice for N->N as somewhat uncommon. It is not present inBishop'sconstructive mathematics, i.e. more or less the setoid model of MLtypetheory. However, it is present in Brouwerian intuitionism and in some realizability models. Brouwer does not have choice for (N->N)->N.Martin Hofmann has some discussion on choice and extensionality inhis thesis,but uses a syntactic criterion somewhat like the one that you outline.

I alreay realized that I should reread Martin's thesis.

One semantic candidate for X could be `all types have a projectivecover'.This is what is used in realizability theory and what Erik Palmgrentranslated to type theory. A type P is projective if for all f:A->Band everyfunction g:P->B there is a function h:P->A with f o h = g. Projectivetypes "have choice". The idea is that the projective types areBishop'spre-sets or the types in the setoid construction.

I'll think about this. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.