eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-03
16
30
10.4230/LIPIcs.CSL.2012.16
article
A Syntactical Approach to Weak omega-Groupoids
Altenkirch, Thorsten
Rypacek, Ondrej
When moving to a Type Theory without proof-irrelevance the notion of a setoid has to be generalized to the notion of a weak omega-groupoid. As a first step in this direction we study the formalisation of weak omega-groupoids in Type Theory. This is motivated by Voevodsky's proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak omega-groupoid.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol016-csl2012/LIPIcs.CSL.2012.16/LIPIcs.CSL.2012.16.pdf
Type Theory
Category Theory
Higher dimensional structures