flâneur

[1611.02108] Cubical Type Theory: a constructive interpretation of the univalence axiom

arxiv.org · 628 words · saved by 1 readers

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs. arXiv Operational Status Get status notifications via email or slack

[1611.02108] Cubical Type Theory: a constructive interpretation of the univalence axiom Skip to main content arXiv is now an independent nonprofit! Learn more × Search arXiv Press Enter to search · Advanced search --> Computer Science > Logic in Computer Science arXiv:1611.02108 (cs) [Submitted on 7 Nov 2016] Title: Cubical Type Theory: a constructive interpretation of the univalence axiom Authors: Cyril Cohen , Thierry Coquand , Simon Huber , Anders Mörtberg View a PDF of the paper titled Cubical Type Theory: a constructive interpretation of the univalence axiom, by Cyril Cohen a

related reading