Cubical type theory

In mathematical logic and theoretical computer science, cubical type theory is a flavor of type theory which gives a computational interpretation to univalent foundations (also known as homotopy type theory).

In cubical type theory, function extensionality and univalence are not postulated as axioms, but rather can be proved as theorems. Unlike traditional homotopy type theory, where the postulate of univalence creates stuck closed terms, cubical type theory has the canonicity property.¹ It also enjoys normalization.²³

This is achieved by adding geometric primitives to the core rules of the type theory, including a formal interval object, interval variables, and operations for filling partial cubes.

The earliest cubical type theory is CCHM cubical type theory, named after its inventors Cohen, Coquand, Huber and Mörtberg.⁴ Later variants include Cartesian cubical type theory.⁵⁶

Cubical type theories have semantics in various types of cubical sets.

The Agda proof assistant includes an implementation of cubical type theory.⁷⁸