Universitat Autònoma de Barcelona
We show that the classifying category C(T)of a dependent type theory T with axioms for identity types admits a nontrivial weak factorisation system. After characterising this weak factorisation system explicitly, we relate it to the homotopy theory of groupoids.
Article
Prepublicació
English
Centre de Recerca Matemàtica
Centre de Recerca Matemàtica. Prepublicacions ;
open access
Aquest document està subjecte a una llicència d'ús Creative Commons. Es permet la reproducció total o parcial, la distribució, i la comunicació pública de l'obra, sempre que no sigui amb finalitats comercials, i sempre que es reconegui l'autoria de l'obra original. No es permet la creació d'obres derivades.
https://creativecommons.org/licenses/by-nc-nd/2.5/
