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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, E-ISSN 1879-2294, 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
Identifiers
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: 2017-12-13Bibliographically 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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 400 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf