Hi Bas & everybody else,

`I do indeed think that Observational Type Theory with quotient types should`

`be the language of a Predicative Topos. I don't see in the moment that the`

`setoid model would introduce anything which isn't provable in the Type`

`Theory and at least in the moment I don't see how to prove the countable`

`axiom of choice in OTT. Bas, could you explain, please?`

`Maybe it is a good idea to give some background to the other people on this`

`mailing list - I give it a try. Please correct me, if necessary.`

`Clearly the following version of the axiom of choice is easily provable in`

`Type Theory and hence also in OTT:`

f : Pi a:A.Sigma b:B.R a b ----------------------------------------------- ac f : Sigma f:A -> B.Pi a:A.R a (f a)

`Indeed, we only use basic properties of Sigma-types. This is not the axiom`

`of choice Bas is referring to.`

`In Topos Theory a proposition is a subobject of 1 (the terminal object) and`

`in Type Theory this corresponds to a type which has at most one inhabitant`

`(i.e. Pi a,b:A.a = b). Let's write Prop for the universe of those`

`propositional types. Now 0,1:Prop and if A:Type and P : A -> Prop then Pi`

`a:A.P a:Prop and hence Pi corresponds to Forall. However, this doesn't work`

`for Sigma since we can project out the witness. We can fix this using a box`

`(or smashing) operator: If A:Type then [A]:Prop. Using quotient types we`

`can actually define [A] = A/~ where ~ : A -> A -> Prop is the trivial`

`relation a ~ b = 1. We now can introduce existential quantification as Ex`

`a:A.P a = [Sigma a:A.P a] : Prop. This gives rise to another version of ac`

`(assuming that R : A -> B -> Prop)`

f : Forall a:A.Ex b:B.R a b ----------------------------------------------- ac' f : Ex f:A -> B.Forall a:A.R a (f a) this expands to f : Pi a:A.[Sigma b:B.R a b] ------------------------------------------------- ac' f : [Sigma f:A -> B.Pi a:A.R a (f a)]

`Note that this is not completely unreasonable: we observe the hidden choice`

`made by f, but we compensate by this by hiding our knowledge. However,`

`Diaconescu has shown that in Topos Theory ac' implies the excluded middle.`

`This shows also that it cannot be derivable in OTT. Btw there is a nice COQ`

`formalisation of Diaconescu's argument, using some unprovable assumptions,`

`obviously. See http://coq.inria.fr/library/Coq.Logic.Diaconescu.html`

`If A is finite we can prove ac', just consider A=2 then this boils down to`

`(ignoring R for the moment) constructing`

p : [B]^2 -------------------- h p : [B^2] We can do this as follows: note that [..] is a monad with return : A -> [A] p : [A]; f : A -> [B] ---------------------- p >>= f : [B] Note that B^2 = BxB. We we construct h p = fst p >>= \ a.snd p >>= \b. return (a,b)

`where fst and snd are the projections. Now Bas seems to be saying that we`

`can also do this if A=Nat, i.e. we can construct`

p : Nat -> [A] -------------------------- h' p : [Nat -> A]

`But I can't see how to do this, but maybe I miss a trick. Are you`

`suggesting a construction which only works in the setoid model?`

Cheers, Thorsten On Jan 29 2007, Bas Spitters wrote:

Dear Thorsten, Robin,Now that the discussion has turned to setoids and observational typetheory, I could not help myself from responding. (Thorsten and I hadquite some off-line discussion about this).I generally agree with Thorsten's description of observational typetheory as internalizing the setoid construction. One clearly feels theneed for such machinery when working with Coq. (Although this seems tohave improved somewhat with the inclusion of the new setoid_rewritetactic.)However, I would like to point out that there seems to be an importantdistinction between the category of setoids and the extensional typetheory defined by observational type theory. Let me first say how theyare similar. Both of these categories should have the structure of a"predicative topos". The search for the right definition of a predicativeanalogue of topos theory was started by Moerdijk and Palmgren. A topos isa model of higher-order intuitionistic logic. We should havetopos pred. topos -------- == --------- iHOL ext type theoryHowever, predicative toposes should also generalize toposes. Currently,the notion of a Pi W-pretopos seems to be a good candidate for the notionof "predicative topos". In any case, observational type theory shouldgive rise to the internal type theory of a predicative topos.However, the predicative topos of setoids models the axiom of countable(dependent) choice. This implies that the Dedekind real numbers and theDedekind real numbers coincide. For general (predicative) toposes theDedekind construction of real numbers and the Cauchy definition of realnumbers need not be the same. Since it is unlikely that observationaltype theory includes the axiom of countable choice we will have to takethis into account when programming, say, the real numbers in epigram.To conclude, when using the setoid construction in intensional typetheory we can use all the results from Bishop's constructive mathematicswhen programming/proving. This is no longer the case in observationaltype theory. Hopefully, it is possible to develop a good replacement.BasPS: I know this may sound too theoretical to some, but it seems to havea real effect on programming, say, real numbers in epigram.------------------------------------------------------- Research GroupFoundations/ Institute for Computing and Information Sciences RadboudUniversity Nijmegen www.cs.ru.nl/~spitters/

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.