On cubical homotopy type theory implemented in the proof assistant Cubical Agda:
Andrea Vezzosi, Anders Mörtberg and Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, 2019 (pdf
Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal, Ale? Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, (arXiv:1606.05223)
Created on June 9, 2022 at 12:23:26. See the history of this page for a list of all contributions to it.