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 type theory, I could not help myself from responding. (Thorsten and I had quite some off-line discussion about this).

I generally agree with Thorsten's description of observational type theory as internalizing the setoid construction. One clearly feels the need for such machinery when working with Coq. (Although this seems to have improved somewhat with the inclusion of the new setoid_rewrite tactic.)

However, I would like to point out that there seems to be an important distinction between the category of setoids and the extensional type theory defined by observational type theory. Let me first say how they are similar. Both of these categories should have the structure of a "predicative topos". The search for the right definition of a predicative analogue of topos theory was started by Moerdijk and Palmgren. A topos is a model of higher-order intuitionistic logic. We should have

        topos           pred. topos
        --------   ==  ---------
        iHOL            ext type theory

However, predicative toposes should also generalize toposes. Currently, the notion of a Pi W-pretopos seems to be a good candidate for the notion of "predicative topos". In any case, observational type theory should give 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 the Dedekind real numbers coincide. For general (predicative) toposes the Dedekind construction of real numbers and the Cauchy definition of real numbers need not be the same. Since it is unlikely that observational type theory includes the axiom of countable choice we will have to take this into account when programming, say, the real numbers in epigram.

To conclude, when using the setoid construction in intensional type theory we can use all the results from Bishop's constructive mathematics when programming/proving. This is no longer the case in observational type theory. Hopefully, it is possible to develop a good replacement.

Bas

PS: I know this may sound too theoretical to some, but it seems to have a real effect on programming, say, real numbers in epigram.

------------------------------------------------------- Research Group Foundations/ Institute for Computing and Information Sciences Radboud University 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.


Reply via email to