文章基本信息

标题：Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
本地全文：下载
作者：Carlo Angiuli ; Kuen-Bang {Hou ; Robert Harper 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：119
页码：1-17
DOI：10.4230/LIPIcs.CSL.2018.6
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.
关键词：Homotopy Type Theory; Two-Level Type Theory; Computational Type Theory; Cubical Sets