The identity type weak factorisation system

Nicola Gambino*, Richard Garner

*Corresponding author for this work

Research output: Contribution to journalArticle

48 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)94-109
Number of pages16
JournalTheoretical Computer Science
Volume409
Issue number1
DOIs
Publication statusPublished - 6 Dec 2008
Externally publishedYes

Keywords

  • Dependent type theory
  • Identity type
  • Weak factorisation system

Fingerprint Dive into the research topics of 'The identity type weak factorisation system'. Together they form a unique fingerprint.

Cite this