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.[1] It also enjoys normalization.[2][3]
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.[4] Later variants include Cartesian cubical type theory.[5][6]
Cubical type theories have semantics in various types of cubical sets.
The Agda proof assistant includes an implementation of cubical type theory.[7][8]
See also
References
- ↑ Huber, Simon (2019). "Canonicity for cubical type theory". Journal of Automated Reasoning 63: 173–210. doi:10.1007/s10817-018-9469-1.
- ↑ Sterling, Jonathan; Angiuli, Carlo (2021). "Normalization for cubical type theory". 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021). pp. 1–15. doi:10.1109/LICS52264.2021.9470719.
- ↑ Sterling, Jonathan (2021). First steps in synthetic Tait computability: the objective metatheory of cubical type theory (Thesis). doi:10.5281/zenodo.5709837.
- ↑ Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). "Cubical type theory: a constructive interpretation of the univalence axiom". 21st International Conference on Types for Proofs and Programs (TYPES 2015). doi:10.4230/LIPIcs.TYPES.2015.5.
- ↑ Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Kuen-Bang, Hou (Favonia); Licata, Daniel R. (2021). "Syntax and models of Cartesian cubical type theory". Mathematical Structures in Computer Science 31 (4): 424–468. doi:10.1017/S0960129521000347.
- ↑ Angiuli, Carlo (2019). Computational semantics of Cartesian cubical type theory (PDF) (Thesis).
- ↑ "Cubical". https://agda.readthedocs.io/en/latest/language/cubical.html.
- ↑ Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas (2021). "Cubical Agda: a dependently typed programming language with univalence and higher inductive types". Journal of Functional Programming 31: e8. doi:10.1017/S0956796821000034.
 |  |
