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