Cubical Type Theory

Contents
References
- Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal. Unifying Cubical and Multimodal Type Theory. 2022.
- Brandon Doherty, Chris Kapulkin, Zachery Lindsey, Christian Sattler. Cubical Models of (∞, 1)-Categories. 2022.
- Hugo Moeneclaey. Parametricity and Semi-Cubical Types. 2022.
- Thierry Coquand, Simon Huber, Christian Sattler. Canonicity and Homotopy Canonicity for Cubical Type Theory. 2022.
- Bruno Bentzen. Naive Cubical Type Theory. 2021.
- Jonathan Sterling, Carlo Angiuli. Normalization for Cubical Type Theory. 2021.
- Evan Cavallo, Robert Harper. Internal Parametricity for Cubical Type Theory. 2021.
- Thomas Streicher, Jonathan Weinberger. Simplicial Sets Inside Cubical Sets. 2021.
- Evan Cavallo, Anders Mörtberg, Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. 2020.
- Ian Orton, Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. 2018.
- Thierry Coquand, Simon Huber, Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. 2018.
- Simon Huber. Canonicity for Cubical Type Theory. 2017.
- Marc Bezem, Thierry Coquand, Simon Huber. The Univalence Axiom in Cubical Sets. 2017.
- Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. 2016.
- Daniel R. Licata, Guillaume Brunerie, A Cubical Approach to Synthetic Homotopy Theory, 2015
- Anders Mörtberga, Cubical Methods in Homotopy Type Theory and Univalent Foundations, 2019
- Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, Daniel R. Licata, Cartesian Cubical Type Theory, 2019
- Carlo Angiuli, Computational Semantics of Cartesian Cubical Type Theory, 2019
- Evan Cavallo, Anders Mörtberg, Andrew W Swan, Unifying Cubical Models of Univalent Type Theory, 2019
- Anders Mörtberg, Loïc Pujet, Cubical Synthetic Homotopy Theory, 2020