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.
Bas
