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