2008/03/31 by Nicola Gambino, Richard Garner · 107 citations
Mathematics · #Advanced Topics in Algebra #Algebra over a field #Algebraic structures and combinatorial models #Algorithm #Artificial intelligence #Axiom #Class (philosophy) #Computer science #Discrete mathematics #Factorization #Geometry #Homotopy #Homotopy and Cohomology in Algebraic Topology #Identity (music) #Mathematics #Pure mathematics #Type (biology) #Type theory #math.CT #math.LO #msc:03B15 #msc:18B40 #msc:18C50
paper · pdf · doi:10.1016/j.tcs.2008.08.030
published in Theoretical Computer Science 409(1), 94-109 (Elsevier BV) · 25 pages; accepted for publication in Theoretical Computer Science
arxiv created 2008/09/01 · openalex publication_date 2008/09/03 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.