Weak omega-categories from intensional type theory

Abstract

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.

References in corpus (3)

• The identity type weak factorisation system
• Two-dimensional models of type theory
• Homomorphisms of higher categories

Cited by in corpus (13)

• Univalence in locally cartesian closed infinity-categories
• A Cubical Language for Bishop Sets
• A type theory for synthetic $\infty$-categories
• Constructing Higher Inductive Types as Groupoid Quotients
• Bicategorical type theory: semantics and syntax
• Note on the construction of globular weak omega-groupoids from types, topological spaces etc
• Univalence in Higher Category Theory
• A proposition is the (homotopy) type of its proofs
• Naive cubical type theory
• Polynomials in homotopy type theory as a Kleisli category
• Globular Multicategories with Homomorphism Types
• Hom weak $\omega$-categories of a weak $\omega$-category
• Segal-type models of higher categories