The HoTT Library: A Formalization of Homotopy Type Theory in Coq

Abstract : We report on the development of the HoTT library, a formal- ization 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 interac- tion of homotopy type theory with recently introduced fea- tures of Coq, such as universe polymorphism and private in- ductive types.
Type de document :
Communication dans un congrès
CPP'17, Jan 2017, Paris, France. ACM, pp.9, CPP'17. 〈10.1145/3018610.3018615〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01421212
Contributeur : Matthieu Sozeau <>
Soumis le : mercredi 21 décembre 2016 - 19:10:55
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Lien texte intégral

Identifiants

Collections

Citation

Andrej Bauer, Gross Jason, Peter Lumsdaine, Michael Shulman, Matthieu Sozeau, et al.. The HoTT Library: A Formalization of Homotopy Type Theory in Coq. CPP'17, Jan 2017, Paris, France. ACM, pp.9, CPP'17. 〈10.1145/3018610.3018615〉. 〈hal-01421212〉

Partager

Métriques

Consultations de la notice

237