Cubical type theory

Cubical type theory is a homotopy type theoryA note on "a homotopy type theory": While we often speak of "homotopy type theory" as a single concept, HoTT is not one single type theory, but a family of related type theories ([cite:@1lab]). This situation is identical to the way we speak of "type theory" as a single field, despite there being many, many different concrete type theories: System F, the simply-typed λ-calculus, any one instance of Martin-Löf type theory, etc. with a primitive unit interval type. Functions out of this interval type are used to define path types and higherI.e. paths (or lines), paths between paths (homotopies or squares), paths between paths between paths (or cubes). path types thereupon.[cite:@thenlabcubicala]