Cubical Agda
From MaRDI portal
Cited in
(19)- lens
- UniMath
- Celf
- cubicaltt
- RedPRL
- HoTTSQL
- Monomorphic Monad
- Regex_Equivalence
- cart-cube
- Constructing higher inductive types as groupoid quotients
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Syntax and models of Cartesian cubical type theory
- On the Nielsen-Schreier theorem in homotopy type theory
- Quotients of bounded natural functors
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- A cubical language for Bishop sets
- Quotients, inductive types, and quotient inductive types
- Quotients by idempotent functions in Cedille
- Representing continuous functions between greatest fixed points of indexed containers
This page was built for software: Cubical Agda
