Homotopy Type Theory in Lean
arXiv:1704.06781 · doi:10.1007/978-3-319-66107-0_30
Abstract
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.
17 pages, accepted for ITP 2017
References in corpus (1)
Cited by in corpus (7)
- Internalizing Representation Independence with Univalence
- On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
- A formal proof of Hensel's lemma over the p-adic integers
- The RedPRL Proof Assistant (Invited Paper)
- Constructing Higher Inductive Types as Groupoid Quotients
- Formalizing the Solution to the Cap Set Problem
- Cellular Cohomology in Homotopy Type Theory