2026-10-15T01:51:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9673 2024-03-06T09:44:47Z ddc:004 open_access

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities Angiuli, Carlo Hou (Favonia), Kuen-Bang Harper, Robert Homotopy Type Theory Two-Level Type Theory Computational Type Theory Cubical Sets 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Carlo Angiuli and Kuen-Bang Hou (Favonia) and Robert Harper 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.6 urn:nbn:de:0030-drops-96734 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6 eng https://creativecommons.org/licenses/by/3.0/legalcode