Types are weak omega-groupoids

Abstract

We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the tower of iterated identity types over that type. We show that the omega-categories arising in this way are in fact omega-groupoids.

28 pages; v2: final journal version

Cited by in corpus (9)

• Univalence for inverse diagrams and homotopy canonicity
• Homotopy limits in type theory
• Topological Quantum Gates in Homotopy Type Theory
• Free Higher Groups in Homotopy Type Theory
• Bicategorical type theory: semantics and syntax
• A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
• Homotopical inverse diagrams in categories with attributes
• On the $\infty$-topos semantics of homotopy type theory
• Monoidal weak omega-categories as models of a type theory