Re: equality is beautiful

[Michael Shulman <shulman@math.uchicago.edu>]

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