Hi Thorsten and others,

On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:
> 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?

Assuming that OTT is the internal type theory of a predicative topos, say a 
PiW-pretopos (which it seems to be the case), it is not possible to prove 
countable choice in OTT. The simple reason is that every topos is a 
PiW-pretopos and that countable choice(CAC) does not hold in the topos of 
sheaves over the reals. Therefore CAC can not hold in the internal type 
theory (i.e. OTT).

Now consider the setoid model. The crucial observation is that the setoid 
Nat=(N,=_Nat) carries the finest possible equality. 
Let X=(X',=_X) be a setoid.
If we know:
     forall n in Nat there exists x in X such that (R n x), 
then, by the construction of the setoid model, there is a function on the 
underlying types f:N->X' such that 
        forall n, (R n (f n))
because Nat carries the finest equality f lifts to a function on the setoid 
level since:
        If n=_Nat m, then (f n)=_X (f m).
Write f':Nat => X for this lifted function. Then 
        forall n in Nat, (R n (f' n)).
Thus proving countable choice in the setoid model.

This is a well-known argument in Bishop's constructive mathematics. Bishop's 
treatment of sets lead to the development of setoids by Hofmann. The lecture 
notes of the TYPES summer school in Chalmers by Erik Palmgren give a nice 
presentation of Bishop set theory in type theory.


Reply via email to