uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
The identity type weak factorisation system
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics.
2008 (English)In: Theoretical Computer Science, ISSN 0304-3975, Vol. 409, no 1, 94-109 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2008. Vol. 409, no 1, 94-109 p.
Keyword [en]
Dependent type theory, Identity type, Weak factorisation system
National Category
Computer Science
URN: urn:nbn:se:uu:diva-106983DOI: 10.1016/j.tcs.2008.08.030ISI: 000261624500005OAI: oai:DiVA.org:uu-106983DiVA: diva2:227526
Available from: 2009-07-15 Created: 2009-07-15 Last updated: 2009-07-15Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Department of Mathematics
In the same journal
Theoretical Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 138 hits
ReferencesLink to record
Permanent link

Direct link