Abstract
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments.We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
| Original language | English |
|---|---|
| Title of host publication | CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017 : CPP 2017 |
| Editors | Yves Bertot, Viktor Vafeiadis |
| Number of pages | 9 |
| Place of publication | New York, NY, USA |
| Publisher | Association for Computing Machinery |
| Publication date | 16 Jan 2017 |
| Pages | 164-172 |
| ISBN (Print) | 978-1-4503-4705-1 |
| ISBN (Electronic) | 9781450347051 |
| DOIs | |
| Publication status | Published - 16 Jan 2017 |
| Event | The 6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017 Conference number: 6 http://cpp2017.mpi-sws.org/ |
Conference
| Conference | The 6th ACM SIGPLAN Conference on Certified Programs and Proofs |
|---|---|
| Number | 6 |
| Country/Territory | France |
| City | Paris |
| Period | 16/01/2017 → 17/01/2017 |
| Internet address |
Keywords
- Coq
- Higher inductive types
- Homotopy type theory
- Univalent foundations
- Universe polymorphism