Hi Robin,

The paper says "Observational reasoning can be simulated in Intensional
Type 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 an
explicit 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.


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 contrasted
with ITT suggests that it should. I must be misunderstanding something.


Reply via email to