| title |
|---|
Cubical type theory |
Cubical 1Lab is great resource.
- 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