The HoTT/HoTT Library in Coq: Designing for Speed. The HoTT/HoTT library is one of the major Coq libraries exploring univalent foundations and homotopy type theory, the other being UniMath. The library includes formalization of the basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions, and quotients, a formalization of modalities (reflective subtoposes) using modules as a way to quantify over all universe levels, formalizations of Cantor spaces and the surreals, the basic theory of h-levels, and a significant amount of category theory centered around comma categories and functoriality of various constructions involving comma categories. A significant amount of work has gone into ensuring that the library compiles quickly. This talk will discuss the various constructions in the HoTT library, as well as the design choices and features, both of Coq and of univalent type theory, which allow our library to compile and typecheck quickly.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- van Doorn, Floris; von Raumer, Jakob; Buchholtz, Ulrik: Homotopy type theory in Lean (2017)
- Krzysztof Bar, Aleks Kissinger, Jamie Vicary: Globular: an online proof assistant for higher-dimensional rewriting (2016) arXiv
- Shulman, Michael: Idempotents in intensional type theory (2016)