Re: equality is beautiful

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

Richard Garner wrote:

>however, if one wishes this notion of product
>to become a special case of the notion of limit (a demand
>which seems not unreasonable) then it is enough to ask your
>type theory to have identity types: for then any preset A can
>be made into a category A# whose hom-setoids are the identity
>types Id_A(x,y) equipped with their propositional equality.

And as well, any preset is thus made into a set(oid).
(Categorially, we form the free set on a given preset.)
And so any category is strict.

Although this is a feature of most type theories in practice,
I've always found it rather artificial.  Bishop's insight
is that you have to *define* equality, and while it's a step up
to say that you *can* define equality if you wish to,
it's unsatisfying to fall back and say you don't *have* to.

Not that identity types can't have their own interesting structure.
The elements of identity types have their own identity types, etc,
so every type becomes not only a set but an infinity-groupoid;
see Awodey & Warren's paper at http://arxiv.org/abs/0709.0248
and Michael Warren's PhD thesis at http://aix1.uottawa.ca/~mwarren/Papers/

But in the philosophical mode where I avoid evil in category theory,
I don't see the justification for identity types in general.


--Toby


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