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)
Magnus Baunsgaard Kristensen?, Rasmus Ejlers Møgelberg, Andrea Vezzosi, Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks (arXiv:2102.01969)
Last revised on September 12, 2022 at 15:53:56. See the history of this page for a list of all contributions to it.