The identity type weak factorisation system Export

@article{citeulike:5289527, 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.}, address = {Essex, UK}, author = {Gambino, Nicola and Garner, Richard}, citeulike-article-id = {5289527}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1458922}, citeulike-linkout-1 = {http://dx.doi.org/10.1016/j.tcs.2008.08.030}, doi = {10.1016/j.tcs.2008.08.030}, issn = {0304-3975}, journal = {Theor. Comput. Sci.}, keywords = {categories, n-cats, type-theory}, number = {1}, pages = {94--109}, posted-at = {2009-07-28 11:22:33}, priority = {5}, publisher = {Elsevier Science Publishers Ltd.}, title = {The identity type weak factorisation system}, url = {http://dx.doi.org/10.1016/j.tcs.2008.08.030}, volume = {409}, year = {2008} }

TY - JOUR ID - citeulike:5289527 L3 - citeulike-article-id:5289527 N2 - 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. IS - 1 JF - Theor. Comput. Sci. SN - 0304-3975 AD - Essex, UK EP - 109 TI - The identity type weak factorisation system PB - Elsevier Science Publishers Ltd. VL - 409 SP - 94 KW - categories KW - n-cats KW - type-theory AU - Gambino, Nicola AU - Garner, Richard PY - 2008/// UR - http://dx.doi.org/10.1016/j.tcs.2008.08.030 ER -