LIPIcs.CSL.2012.16.pdf
- Filesize: 0.54 MB
- 15 pages
Document
A Syntactical Approach to Weak omega-Groupoids
Authors
-
Part of:
Volume:
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (CSL 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-09-03
Cite AsGet BibTex
Thorsten Altenkirch and Ondrej Rypacek. A Syntactical Approach to Weak omega-Groupoids. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 16-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.CSL.2012.16
https://doi.org/10.4230/LIPIcs.CSL.2012.16
Abstract
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.
Keywords
- Type Theory
- Category Theory
- Higher dimensional structures
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads