文章基本信息

标题：Decomposing the Univalence Axiom
本地全文：下载
作者：Ian Orton ; Andrew M. Pitts
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：104
页码：1-19
DOI：10.4230/LIPIcs.TYPES.2017.6
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.
关键词：dependent type theory; homotopy type theory; univalent type theory; univalence; cubical type theory; cubical sets