To rephrase what Toby said: the construction of limits via products and equalizers only works for limits over a domain category which has a set(oid) of objects (what Toby calls a "strict category"), whether that set is large or small. Of course, it also only works when the products and equalizers exist; a particular limit may exist without the relevant products and equalizers existing. It is true that we are most interested in limits over small strict categories, but there are many limits over large categories that do exist and are occasionally useful. For instance, every object X of a category C is the limit of the identity functor C --> C weighted by the representable weight hom_C(X,-), whether or not C is small or strict. Of course, by Freyd's theorem, a large category cannot have large *products* unless it is a preorder, so one shouldn't expect to be able to construct such large limits via products and equalizers. This matches quite nicely with the type-theoretic philosophy, according to which the large categories which arise in nature are rarely strict, so that it wouldn't even make sense to ask for the relevant products and equalizers. Mike Toby Bartels wrote:

David Leduc wrote:

...

What about the characterization of limits in terms of products and equalizers? It states that the limit of a functor F:J->C is constructed by products indexed by the set(oid) of objects and the set(oid) of arrows of J. But if you don't allow equality on objects in J, you only have a preset of objects, not a set(oid).

Consider the analogy between small and strict categories. (A category is strict if it is equipped with a notion of equality of objects. Logically, this is a structure rather than a property like smallness.)

Often when speaking of small categories, one speaks relative to a universe which is a collection of set(oid)s or a collection of set(oid) cardinalities, so every small preset automatically comes equipped with a notion of equality. In this case, every small category is strict. Conversely, every strict category is small relative to some universe, if you accept an axiom such as Grothendieck's axiom of universes. So these are very closely related concepts.

As is well known, we are most interested in the limit of F: J -> C for small J. Less well known, but also true, we are most interested in it when J is strict. In that case, there is no problem; the arrows of J form a set(oid), and we can consider products indexed by that set(oid). In principle, J doesn't have to be strict, any more than it has to be small, but if you have some reason to believe that the limit exists, then you can examine that reason to see what product is relevant. Most of the time, you can just assume that J is small and strict.

--Toby

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

On Sun, Mar 21, 2010 at 2:36 PM, Toby Bartels <toby+categories@ugcs.caltech.edu> wrote:

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/

I think maybe the papers you wanted to refer to for that fact are Benno van den Berg and Richard Garner, Types are weak ω-groupoids, arXiv:0812.0298 Peter Lumsdaine, Weak ω-categories from intensional type theory, arXiv:0812.0409 The Awodey+Warren papers are about the other direction, that type theory with identity types can be interpreted in any well-enough-behaved model category. I agree, though, that identity types vitiate the goal of doing category theory without a notion of equality for objects. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]