Peter LeFanu Lumsdaine - Weak omega-categories from intensional type theory

lmcs:1062 - Logical Methods in Computer Science, September 17, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:24)2010
Weak omega-categories from intensional type theoryArticle

Authors: Peter LeFanu Lumsdaine

    We show that for any type in Martin-Löf 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.


    Volume: Volume 6, Issue 3
    Published on: September 17, 2010
    Imported on: December 1, 2009
    Keywords: Mathematics - Logic,Mathematics - Category Theory,math.CT

    11 Documents citing this article

    Consultation statistics

    This page has been seen 1255 times.
    This article's PDF has been downloaded 415 times.