Hi Robin,

The paper says "Observational reasoning can be simulated inIntensionalType Theory by the use of setoids, i.e. types with an explicit equivalence relation".I'm not clear on what the differences are between OTT and simulating observational reasoning with setoids in ITT. Clearly OTT has anexplicit equivalence relation (=) which is "polymorphic" over(certain)types. So does the paper mean "explicit" in some other sense?

I am not sure I understand your question. Let my try to answer anyway.

`In Intensional Type Theory one uses setoids to simulate extensional`

`reasoning, a setoid is a type together with an equivalence relation`

`(i.e. you can form the large type SETOID):`

A : * ~_AA : A -> A -> * eqR_A : EquivRel ~ --------------------------------- (A,~_A,eqR_A) : SETOID

`where EquivRel is formalizes that ~ is an equivalence relation. Given`

`setoids AA=(A,~A,eqR_A) and BB = (B,~B,eqR_B) we can form a new`

`setoid AA => BB where the underlying set is given as`

A=>B = Sigma f : A->B . Pi a,b:A.(a ~A b) -> f a ~ f b and the equivalence relation (f,_) ~A=>B (g,_) = Pi a:A.f a ~B g a

`and I leave it as an exercise to show that this is an equivalence`

`relation. Clearly, we can use A => B as if it were the function space`

`and ~ as if it were the propositional equality on the function type.`

`However, each time we want to substitute an extensionally equal`

`function by another one, we still have to prove that our predicate`

`preserves the setoid equality. This seems unnessessary because we`

`know that all predicates we can define preserve extensional equality.`

`In a different way this also applies to quotient types. While in`

`general not all function preserve the equality we quotient by, we can`

`introduce an elimination operator for quotients which requires us to`

`show that the operation preserves the equality. If this is the only`

`way we ever use quotient types we also know that any predicate will`

`preserve the equality.`

`E.g. if we want to formalize category theory we would like to define`

`a category simply as a structure:`

Obj : * Hom : Obj -> Obj -> * id : Pi A:Obj.Hom A A comp : Pi A,B,C:Hom B C -> Hom A B -> Hom A c eqL : Pi A,B:*;f:Hom A B.comp f (id A) = f ...

`However, we want be able to construct many categories this way,`

`because the equality we want to use may not be the propositional`

`equality of Intensional Type Theory. E.g. if we formalize the`

`category of groups a morphism is a function on the underlying sets`

`which commutes with the group structure. Hence for two morphisms to`

`be equal requires to show that they use the same proof that the`

`function commutes with the group structure!?`

`Hence we certainly should introduce a setoid of Homsets. Some people`

`have suggested that this is sufficent, however, in this setting it is`

`not clear how to perform certain constructions which turn homsets`

`into objects, such as the construction of the arrow category (objects`

`are morphisms, morphisms are commuting squares). It would be`

`consequent to use a setoid to model objects as well. Fine, however,`

`we now have to make precise that homsets are a family of setoids`

`indexed by a setoid. In particular we have to provide a family of`

`isomorphisms which assigns to equal objects an isomorphism of`

`homesets...`

`All this can be done, but it seems that we are reinventing Type`

`Theory on the level of setoids. An indeed this basically the idea of`

`OTT: to use a model construction to interpret all constructions of`

`Type Theory as taking place in the setoid interpretation. The`

`advantage is that you can use the setoid equality in the model in the`

`same way as you use propositional equality in ordinary Type Theory.`

`I.e. we use the relation ~A=>B as defined above but we never have to`

`show that our predicates respect this relation because this is part`

`of our model construction (or more exactly part of our defintion what`

`it means to be a predicate over A=>B). In the category theory example`

`we can just use the naive formalisation, but since we can use`

`arbitrary quotients we get all the categories we are interested in.`

`So to summarize: OTT can be viewed as a convenient interface to use`

`setoids without having to realize all the underlying machinery. It's`

`goal is to have an extensional propositional equality but to retain`

`decidability and canonicity.`

Cheers. Thorsten

And doesn't OTT have the same problems (equality not automatically substitutive, complications in formalising category theory, lots of explicit coercions) that the paper says ITT has? I don't see how OTT helps with any of those problems, but the way that OTT is contrastedwith ITT suggests that it should. I must be misunderstandingsomething.-- Robin