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