Cubical Agda

MaRDI QIDQ1350644swMATHFDO

Official website https://doi.org/10.1145/3342524

Source code repository https://github.com/agda/cubical

Cited in

(19)

• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• Quotients, inductive types, and quotient inductive types
• Constructing higher inductive types as groupoid quotients
• lens
• UniMath
• Celf
• cubicaltt
• RedPRL
• HoTTSQL
• Monomorphic Monad
• Regex_Equivalence
• cart-cube
• scientific article; zbMATH DE number 7407785 (Why is no real title available?)
• scientific article; zbMATH DE number 7471707 (Why is no real title available?)
• scientific article; zbMATH DE number 7471712 (Why is no real title available?)
• Quotients by idempotent functions in Cedille
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Syntax and models of Cartesian cubical type theory

This page was built for software: Cubical Agda