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]
@article{CohenCHM17,
title = {Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom},
author = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders Mörtberg},
year = {2017},
url = {http://collegepublications.co.uk/ifcolog/?00019},
researchr = {https://researchr.org/publication/CohenCHM17},
cites = {0},
citedby = {0},
journal = {FLAP},
volume = {4},
number = {10},
pages = {3127-3170},
}