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/ ]