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.
|Original language||English (US)|
|Title of host publication||Computer Science Logic 2018, CSL 2018|
|Editors||Dan R. Ghica, Achim Jung|
|Publisher||Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing|
|State||Published - Aug 1 2018|
|Event||27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom|
Duration: Sep 4 2018 → Sep 7 2018
|Name||Leibniz International Proceedings in Informatics, LIPIcs|
|Conference||27th Annual EACSL Conference Computer Science Logic, CSL 2018|
|Period||9/4/18 → 9/7/18|
Bibliographical noteFunding Information:
Funding This research was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053 and the National Science Foundation through grant DMS-1638352. Any opinions, findings and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of any sponsoring institution, the U.S. government or any other entity.
This author thanks the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken. The program was supported by EPSRC grant number EP/K032208/1.
- Computational type theory
- Cubical sets
- Homotopy type theory
- Two-level type theory