Cited in
(13)- Model structure on the universe of all types in interval type theory
- Naive cubical type theory
- HoTT
- cubicaltt
- RedPRL
- Models of type theory based on Moore paths
- Cubical methods in homotopy type theory and univalent foundations
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Cubical Agda
- Constructive sheaf models of type theory
- Internal universes in models of homotopy type theory
- Syntax and models of Cartesian cubical type theory
- An introduction to univalent foundations for mathematicians
This page was built for software: cart-cube
