Cubical Type Theory: a constructive interpretation of the univalence axiom

Cyril Cohen, Thierry Coquand, Simon Huber +1

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…