The identity type weak factorisation system

Nicola Gambino, Richard Garner

Research output: Contribution to journalArticlepeer-review

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

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