Publications based on the HoTT library

The main publication:

• The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arxiv CPP17

Publications related to parts of the library:

• Formalising real numbers in homotopy type theory, Gaëtan Gilbert PDF CPP17 2017: 112-124
• Experience Implementing a Performant Category-Theory Library in Coq, Jason Gross, Adam Chlipala, David I. Spivak PDF ITP 2014
• Modalities in homotopy type theory, Egbert Rijke, Michael Shulman, Bas Spitters PDF LMCS

Building on top of the library (sources elsewhere):

• Finite Sets in Homotopy Type Theory, Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide (CPP 2018).