1 Feb 08:55 2007

### Re: Definitional equality in observational type theory

Thorsten Altenkirch <txa <at> cs.nott.ac.uk>

2007-02-01 07:55:30 GMT

2007-02-01 07:55:30 GMT

Hi Bas, thank you - indeed this is a very interesting observation. This was the proof I had in mind when I first claimed that the axiom of choice is provable in OTT. However, I was deluded in believing that OTT/ predicative topoi exactly characterize the theory of the setoid model. As you clearly point out this is not the case. To me this is an incompleteness of the formal system (OTT/predicative topoi) wrt the intended interpretation. This should be fixable, leading to OTT+X or predicative topoi + X which should be complete wrt the setoid model. More categorically we could say that X characterizes the predicative topoi obtained by an exact completion of an LCCC - I think. Indeed, in the setoid model we can construct a function f : A -> [B] ------------------ lift f : [A -> B] if the setoid A is "trivial", i.e. has the identity as its equivalence relation. The construction is exactly the one you point out & it actually corresponds to my previous informal explanation why this is "not unreasonable": > Note that this is not completely unreasonable: we observe the > hidden choice made by f, but we compensate by this by hiding our > knowledge. Which setoids have a trivial equality? Certainly all first order types. However, if we start with an extensional theory (which can be(Continue reading)