The Identity type weak factorisation system | Macquarie University ResearchOnline

Home

Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/117351

12 Visitors

13 Hits

0 Downloads

Title: The Identity type weak factorisation system
Related: Theoretical computer science, Vol. 409, No. 1 (2008), p.94-109
DOI: 10.1016/j.tcs.2008.08.030
Publisher: Elsevier
Date: 2008
FoR/RFCD Code(s): 080200 Computation Theory and Mathematics 080300 Computer Software 170200 Cognitive Sciences
Author/Creator: Gambino, Nicola
Author/Creator: Garner, Richard
Description: We show that the classifying category View the MathML source of a dependent type theory View the MathML source 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.
Description: 16 page(s)
Subject Keyword: 080200 Computation Theory and Mathematics
Subject Keyword: 080300 Computer Software
Subject Keyword: 170200 Cognitive Sciences
Subject Keyword: dependent type theory
Subject Keyword: identity type
Subject Keyword: weak factorisation system
Resource Type: journal article
Organisation: Macquarie University. Dept. of Computing

Macquarie University ResearchOnline