Computational Semantics of Cartesian Cubical Type Theory

Dependent type theories are a family of logical systems that serve as expressive functional programming languages and as the basis of many proof assistants. In the past decade, type theories have also attracted the attention of mathematicians due to surprising connections with homotopy theory; the study of these connections,

known as homotopy type theory, has in turn suggested novel extensions to type theory, including higher inductive types and Voevodsky’s univalence axiom. However, in their

original axiomatic presentation, these extensions lack computational content, making them unusable as programming constructs and unergonomic in proof assistants. In this dissertation, we present Cartesian cubical type theory, a univalent type theory that extends ordinary type theory with interval variables representing abstract

hypercubes. We justify Cartesian cubical type theory by means of a computational semantics that generalizes Allen’s semantics of Nuprl [All87] to Cartesian cubical

sets. Proofs in our type theory have computational content, as evidenced by the canonicity property that all closed terms of Boolean type evaluate to true or false. It is the second univalent type theory with canonicity, after the De Morgan cubical type theory of Cohen et al. [CCH M18], and affirmatively resolves an open question of whether Cartesian interval structure constructively models univalent universes.