Cubical Type Theory

References

• Unifying Cubical and Multimodal Type Theory. Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal. 2022.
• Cubical Models of (∞, 1)-Categories. Brandon Doherty, Chris Kapulkin, Zachery Lindsey, Christian Sattler. 2022.
• Parametricity and Semi-Cubical Types. Hugo Moeneclaey. 2022.
• Canonicity and Homotopy Canonicity for Cubical Type Theory. Thierry Coquand, Simon Huber, Christian Sattler. 2022.
• Naive Cubical Type Theory. Bruno Bentzen. 2021.
• Normalization for Cubical Type Theory. Jonathan Sterling, Carlo Angiuli. 2021.
• Internal Parametricity for Cubical Type Theory. Evan Cavallo, Robert Harper. 2021.
• Simplicial Sets Inside Cubical Sets. Thomas Streicher, Jonathan Weinberger. 2021.
• Unifying Cubical Models of Univalent Type Theory. Evan Cavallo, Anders Mörtberg, Andrew W Swan. 2020.
• Axioms for Modelling Cubical Type Theory in a Topos. Ian Orton, Andrew M. Pitts. 2018.
• On Higher Inductive Types in Cubical Type Theory. Thierry Coquand, Simon Huber, Anders Mörtberg. 2018.
• Canonicity for Cubical Type Theory. Simon Huber. 2017.
• The Univalence Axiom in Cubical Sets. Marc Bezem, Thierry Coquand, Simon Huber. 2017.
• Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. 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