RedPRL
From MaRDI portal
Cited in
(11)- HoTT
- UniMath
- cubicaltt
- HoTTSQL
- cart-cube
- Cubical methods in homotopy type theory and univalent foundations
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Meaning explanations at higher dimension
- Cubical Agda
- Syntax and models of Cartesian cubical type theory
- An introduction to univalent foundations for mathematicians
This page was built for software: RedPRL
