The identity type weak factorisation system

Abstract

We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.

25 pages; accepted for publication in Theoretical Computer Science

References in corpus (2)

• Homotopy-theoretic aspects of 2-monads
• Two-dimensional models of type theory

Cited by in corpus (37)

• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Algebraic weak factorisation systems I: accessible AWFS
• The local universes model: an overlooked coherence construction for dependent type theories
• Univalence for inverse diagrams and homotopy canonicity
• Two-dimensional models of type theory
• The Frobenius Condition, Right Properness, and Uniform Fibrations
• Weak omega-categories from intensional type theory
• Homotopy limits in type theory
• Type theory and homotopy
• Homotopy Theoretic Models of Type Theory
• Univalence in locally cartesian closed infinity-categories
• All $(\infty ,1)$-toposes have strict univalent universes
• Towards a constructive simplicial model of Univalent Foundations
• Models of Type Theory with Strict Equality
• The Equivalence Extension Property and Model Structures
• Notes on Clans and Tribes
• Dialectica models of type theory
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
• Models of Martin-Löf type theory from algebraic weak factorisation systems
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• A Topological Application of Labelled Natural Deduction
• The General Universal Property of the Propositional Truncation
• Exact completion of path categories and algebraic set theory -- Part I: Exact completion of path categories
• Cubical sets and the topological topos
• Note on the construction of globular weak omega-groupoids from types, topological spaces etc
• On the $\infty$-topos semantics of homotopy type theory
• Coherence of strict equalities in dependent type theories
• Homotopical inverse diagrams in categories with attributes
• Kripke-Joyal forcing for type theory and uniform fibrations
• Univalence in Higher Category Theory
• A proposition is the (homotopy) type of its proofs
• A category-theoretic version of the identity type weak factorization system
• Identity types and weak factorization systems in Cauchy complete categories
• From Identity to Difference: A Quantitative Interpretation of the Identity Type
• On homotopy exponentials in path categories
• Stable factorization from a fibred algebraic weak factorization system
• Hurewicz fibrations in elementary toposes