RedPRL
From MaRDI portal
Software:35364
swMATH23593MaRDI QIDQ35364FDOQ35364
Author name not available (Why is that?)
Cited In (5)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Cubical methods in homotopy type theory and univalent foundations
- Meaning explanations at higher dimension
- Syntax and models of Cartesian cubical type theory
- An introduction to univalent foundations for mathematicians
This page was built for software: RedPRL