arXiv Analytics

Sign in

arXiv:0812.0409 [math.LO]AbstractReferencesReviewsResources

Weak omega-categories from intensional type theory

Peter LeFanu Lumsdaine

Published 2008-12-02, updated 2010-09-17Version 4

We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

Journal: LMCS 6 (3:24) 2010
Categories: math.LO, math.CT, math.CT
Related articles: Most relevant | Search more
arXiv:1507.03634 [math.LO] (Published 2015-07-13)
Idempotents in intensional type theory
arXiv:1205.5527 [math.LO] (Published 2012-05-24)
Combinatorial realizability models of type theory
arXiv:1202.1012 [math.LO] (Published 2012-02-05, updated 2013-12-03)
Quotient completion for the foundation of constructive mathematics

Links

Toolbox