HoTT
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 13 articles )
Showing results 1 to 13 of 13.
Sorted by year (- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Chapman, James; Uustalu, Tarmo; Veltri, Niccolò: Quotienting the delay monad by weak bisimilarity (2019)
- Kapulkin, Krzysztof; Szumiło, Karol: Internal languages of finitely complete ((\infty, 1))-categories (2019)
- Kirst, Dominik; Smolka, Gert: Categoricity results and large model constructions for second-order ZF in dependent type theory (2019)
- Ladyman, James; Presnell, Stuart: Universes and univalence in homotopy type theory (2019)
- Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
- Grayson, Daniel R.: An introduction to univalent foundations for mathematicians (2018)
- Shulman, Michael: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory (2018)
- Vinogradova, Polina; Felty, Amy P.; Scott, Philip: Formalizing abstract computability: Turing categories in Coq (2018)
- 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)
- Timany, Amin; Jacobs, Bart: Category theory in Coq 8.5 (2016)