Re: equality

[Dusko Pavlovic <dusko@kestrel.edu>]

hi.

several people suggest dependent type theory as a foundation to
formalize categories. maybe it is worth mentioning that per martin-
loef (the originatory of dependent types) worked this out, prolly in
the 70s. that was one of his early examples. many people who
implemented basic category theory in the 80s (burstall-rydeheard,
NuPRL team etc) followed this design. i am sure that there are people
on the list who know much more about this than i do.

while martin-loef's construction is quite natural and easy to
reconstruct, one idea that still seems to be missing here, and leads
to some confusion: the distinction between the extensional equality,
ie term conversion, and the intentional equality, ie equality types.

without going into any details, let me suggest that this formalization
may clarify some confusion.

in martin loef's formalization, the composition operation does not
involve equality: no equality expressions occur in the expression
Hom(A,B) # Hom(B,C) ---> Hom(A,C). what does occur are two copies of
B. but ***being able to copy B is not the same thing as being able to
decide the equality predicate***. mapping things along the diagonal is
not the same thing as being able to decide whether something lies in
the image or not.

in practice, if i give you an object (say a group B) you will have no
problem to make two identical copies of that group, in whichever form
it may be given. but if i give you two big complicated groups, and you
want to know whether they are equal on the nose, then you need to see
how they are represented. in other words, you need to open the black
boxes, and see what exactly are the elements of these groups etc. and
this is not very categorical. as we all know, the whole point of eg
the universal properties is that you describe things without opening
any black boxes.

one more thing, also apparent from any formalization: the reason why
the object equality is no problem for small (internal) categories is
that their objects can be viewed as arrows of the base category (and
the arrows are, of course, in the business of being equal or not).

-- dusko


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