Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

By C. Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Types for Proofs and Programs, 2015

380 citations recorded by the source corpus.

This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

Subfields: Geometry and Topology, Mathematical Physics, Nuclear and High Energy Physics

View Paper: https://www.semanticscholar.org/paper/2a7d8f1a3106ba51d4f70a731b46170c39b41add

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Geometry and Topology

In Mathematical Physics

In Nuclear and High Energy Physics

Citations in the corpus

A type theory for synthetic ∞-categories (2017, methodology): “Formally, our theory is very similar to the recent “cubical type theories” studied by [5] and others, whose basic setup can also be regarded as an instance of ours, using the theory of a de Morgan algebra.”
The Frobenius condition, right properness, and uniform fibrations (2015, methodology): “2, we obtain an awfs (Ct ,F′) whose right maps are exactly the uniform Kan fibrations considered in [11].”