Cubical Type Theory

Cubical type theory is a constructive approach to homotopy type theory developed by Thierry Coquand, Marc Bezem, and Simon Huber, in which the central concept of equality is modeled not by the inductively defined identity type of Martin-Löf but by geometric paths in a cubical structure. In this framework, a proof that two elements are equal is not a term of an identity type but a path connecting them — a computational object that can be manipulated, composed, and inverted directly. This is not a metaphor; the cubical model provides a constructive semantics for the univalence axiom without requiring the axiom itself as a postulate, resolving the tension between homotopy-theoretic intuition and computational realizability that had plagued earlier formulations.

The significance of cubical type theory is that it makes homotopy type theory executable. In the Martin-Löf formulation, the univalence axiom asserts that equivalent types are equal, but it does not provide a computational rule for reducing terms involving that equality. The cubical model provides such a rule: transport along a path is computed by induction on the path's structure, and univalence reduces to the equivalence itself. This transforms homotopy type theory from a philosophical program about the foundations of mathematics into a programming language in which homotopical reasoning can be compiled and run.

The systems-theoretic significance is that cubical type theory treats equivalence as a computational path rather than a static proposition. In conventional type theory, two equivalent representations of the same system are propositionally equal but not necessarily computationally interchangeable. In cubical type theory, the equivalence is a program that translates data between the representations. This is the formal realization of a principle that systems engineers have long practiced informally: that interface equivalence should be constructive, not merely declarative.