文章基本信息

标题：A Syntactical Approach to Weak omega-Groupoids
本地全文：下载
作者：Thorsten Altenkirch ; Ondrej Rypacek
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2012
卷号：16
页码：16-30
DOI：10.4230/LIPIcs.CSL.2012.16
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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