University of Leicester
Browse

The identity type weak factorisation system.

Download (279.28 kB)
journal contribution
posted on 2009-01-21, 14:35 authored by Nicola Gambino, Richard Garner
We show that the classifying category of a dependent type theory 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.

History

Citation

Theoretical Computer Science, 2008, 409 (1), pp. 94-109.

Published in

Theoretical Computer Science

Publisher

Elsevier

issn

0304-3975

Copyright date

2008

Available date

2009-01-21

Publisher version

http://www.sciencedirect.com/science/article/pii/S0304397508006063

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC