A Syntactical Approach to Weak omega-Groupoids
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.
Type Theory
Category Theory
Higher dimensional structures
16-30
Regular Paper
Thorsten
Altenkirch
Thorsten Altenkirch
Ondrej
Rypacek
Ondrej Rypacek
10.4230/LIPIcs.CSL.2012.16
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode