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]
On homotopy canonicity for cubical type theory:
Thierry Coquand, Simon Huber, Christian Sattler: Homotopy canonicity for cubical type theory, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) [doi:10.4230/LIPIcs.FSCD.2019.11, arXiv:1902.06572]
Thierry Coquand, Simon Huber, Christian Sattler: Canonicity and homotopy canonicity for cubical type theory, Logical Methods in Computer Science 18 1 (2022) lmcs:9043 [doi:10.46298/lmcs-18%281%3A28%292022, arXiv:1902.06572]
Last revised on April 10, 2026 at 08:08:22. See the history of this page for a list of all contributions to it.