Cubical Type Theory

Abstract

Cubical type theory is an extension of dependent type theory providing a constructive interpretation of the univalence axiom and higher inductive types by modeling equality as paths over an explicit interval.

Definition

Cubical type theory is a formal system of dependent type theory where types are modeled as cubical sets. We replace the traditional inductive definition of the identity type with a path type constructed via a formal interval object $\mathbb{I}$.

The interval $\mathbb{I}$ contains endpoints $i_0$ and $i_1$. A path between terms $x,y:A$ is a function $p:\mathbb{I}\to A$ satisfying the definitional equalities $p{i}_0\equiv x$ and $p{i}_1\equiv y$.

Higher-dimensional cubes arise naturally as functions from multiple interval variables. For example, a term $q:\mathbb{I}\to \mathbb{I}\to A$ represents a two-dimensional square. To ensure types exhibit the required structure of Kan complexes, we require types to support explicit Kan operations—specifically composition and transport—which compute constructively. This computational behavior resolves the main deficiency of standard Homotopy Type Theory, where the univalence axiom lacks computational content.

See also

Homotopy Type Theory Higher Inductive Type Univalence Principle Kan Complex

References

cohen2018-cubical