cohen2016-cubical-type-theory

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, “Cubical Type Theory: a constructive interpretation of the univalence axiom,” 2016.