Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP, 4(10):3127-3170, 2017. [doi]

Abstract

Abstract is missing.