WEAK omega-CATEGORIES FROM INTENSIONAL TYPE THEORY
We show that for any type in Martin-Lof 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 P(MLId) of definable "composition laws", and give an action of this operad on the terms of any type and its identity types.
omega-categories intensional type theory martin-lof identity types operads category theory higher categories n-categories infinity-categories dependent type theory