On symmetry and introducing the language of homotopy type theory for univalent foundations of mathematics:
Early discussion of cubical type theory with categorical semantics in cubical sets:
Marc Bezem, Thierry Coquand, Simon Huber: A Model of Type Theory in Cubical Sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013) [doi:10.4230/LIPIcs.TYPES.2013.107, pdf]
Marc Bezem, Thierry Coquand, Simon Huber: The univalence axiom in cubical sets, Journal of Automated Reasoning 63 (2019) [doi:10.1007/s10817-018-9472-6, arXiv:1710.10941]
Last revised on April 10, 2026 at 08:01:40. See the history of this page for a list of all contributions to it.