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".## Advertising

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