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.
