Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

Carlo Angiuli, Kuen Bang Hou, Robert Harper

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations


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 languageEnglish (US)
Title of host publicationComputer Science Logic 2018, CSL 2018
EditorsDan R. Ghica, Achim Jung
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Print)9783959770880
StatePublished - Aug 1 2018
Externally publishedYes
Event27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom
Duration: Sep 4 2018Sep 7 2018

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference27th Annual EACSL Conference Computer Science Logic, CSL 2018
CountryUnited Kingdom

Bibliographical note

Funding 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.

Funding Information:
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

Fingerprint Dive into the research topics of 'Cartesian cubical computational type theory: Constructive reasoning with paths and equalities'. Together they form a unique fingerprint.

Cite this