6533b870fe1ef96bd12d0574

RESEARCH PRODUCT

The identity type weak factorisation system

Richard GarnerNicola Gambino

subject

Class (set theory)Pure mathematicsGeneral Computer ScienceDependent type theoryHomotopiaType (model theory)Identity (music)Theoretical Computer Science510 - Consideracions fonamentals i generals de les matemàtiquesCombinatorics18C50Mathematics::Category TheoryFOS: MathematicsCategory Theory (math.CT)Univalent foundationsAxiomMathematicsHomotopy03B15; 18C50; 18B40Mathematics - Category TheoryIdentity type weak factorisation systemMathematics - LogicTipus Teoria dels03B15Type theory18B40Homotopy type theoryLogic (math.LO)Weak factorisation systemIdentity typeComputer Science(all)

description

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.

yearjournalcountryeditionlanguage
2008-12-01
https://dx.doi.org/10.48550/arxiv.0803.4349