Cubical type theory

Cubical 1Lab is great resource.

Links

• Experimental implementation of Cubical Type Theory in which the user can directly manipulate n-dimensional cubes
• Cartesian Cubical Type Theory
• RedPRL - Purpose of RedPRL is to provide a practical implementation of Computational Cubical Type Theory in the Nuprl style, integrating modern advances in proof refinement.
• redtt - Core language for cartesian cubical type theory with extension types.
• cooltt - A cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory.
• Cubical 1Lab - Formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory. (Code)
• Textbook on Cubical Methods