Re: terminology

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

Thorsten Altenkirch wrote:

>Toby Bartels wrote:

[I suggested formalising category theory without equality of objects
in intensional Martin-Löf type theory, Coq, or SEAR without equality]

>I don't know any reasonable formalisation in Intensional Type Theory.
>People usually assume that hom sets are a setoid but objects aren't.
>This means that constructions like arrow categories are not available.
>To avoid this one would have to formalize explicitely what is a family
>of setoids indexed over a setoid. After this it is hard to see the
>category theory...

Why do you say that one cannot construct arrow categories?
We need only dependent sums, which Martin-Löf has in his type theory,
to form the type of all morphisms of a given category C.
We cannot compare these for equality, nor do we want to.
What we do need to compare for equality are commutative squares
(which are the morphisms in the arrow category) with given corners
(actually, even with two given parallel sides), and this we can do.

To be explicit, let Ob be the type of objects of the category C;
given x, y: Ob, let x -> y be the type of morphisms from x to y.
Given further two morphisms f, g: x -> y, we have a proposition f = g.
(Martin-Löf identifies propositions with types, but Coq does not,
so I say "proposition" so you can interpret it in either system.)
Then of course, there are operations and axioms that I will skip,
except to introduce ; as notation for composition in diagrammatic order:
f: x -> y, g: y -> z |- f;g: x -> z.

Then the type of objects of the arrow category of C
is sum_{x:Ob} sum_{y:Ob} x -> y, a dependent sum of dependent sums;
a typical element of this type is (x,y,f), where x,y: Ob and f: x -> y.
Given two objects (x,y,f) and (u,v,g) of the arrow category,
the type of morphisms from (x,y,f) to (u,v,g) is
sum_{a:x->u} sig_{b:y->v} f;b = a;g. (*)
(Again, I say "sig" to keep things correct in Coq,
since then f;b = a;g is a proposition rather than a type;
this is the same as a sum to Martin-Löf.)
A typical element of this type is (a,b,p),
where p is a proof of the relevant equality.

A set theorist might well write (*) above as
{ (a,b) | a: x -> u, b: y -> v, f;b = a;g };
they do not refer to p, since set theorists accept proof irrelevance.
They would then be finished, but as type theorists,
we still need to define when parallel morphisms are equal.
We do this by imposing proof irrelevance in the definition;
that is, the definition of equality makes no reference to p.
Specifically, given parallel morphisms (a,b,p) and (c,d,q),
both from (x,y,f) to (u,v,g) in the arrow category,
we define the proposition that they are equal
to be the conjunction of a = c and b = d.
Notice that this makes sense, since a,c: x -> u and b,d: y -> v.
So we can define that equality which we need in the arrow category.

To sum up:  An object in the arrow category of C is (x,y,f),
where x and y are objects of C and f: x -> y is a morphism of C.
A morphism from (x,y,f) to (u,v,g) in the arrow category of C
is (a,b,p), where a: x -> u, b: y -> v, and p: a;g = f;b.
Finally, two such morphisms (a,b,p) and (c,d,q) are equal
if and only if a = c and b = d.  (I leave it as an exercise
for the reader to define the operations and prove the axioms
that define the arrow category of C as a category.)

If you find the summary above a bit too wordy, say
  A morphism from (x,y,f) to (u,v,g) in the arrow category of C
  is (a,b), where a: x -> u and b: y -> v such that a;g = f;b.
That we do not give a name to the proof that a;g = f;b
makes it obvious what the definition of equality of morphisms should be,
so we leave it out as an abuse of language, or a convention of definition.
If it still seems odd that it is even possible to give a proof a name,
well, that is a feature of Martin-Löf type theory and Coq
that you can ignore (just as I ignore the feature of ZFC
that it is possible to ask whether two arbitrary sets are equal),
but you can also use SEAR without equality to avoid even that.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]