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
• Synthetic topology in homotopy type theory for probabilistic programming, Florian Faissole, Bas Spitters, PDF
• Idempotents in intensional type theory, Michael Shulman, LMCS link

Building on top of the library (sources elsewhere):

• Lawvere-Tierney sheafification in Homotopy Type Theory, Kevin Quirin PDF
• Model structure on the universe in a two level type theory, Simon Boulier, Nicolas Tabareau PDF 2016
• Finite Sets in Homotopy Type Theory, Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide (CPP 2018).
• A HoTT Quantum Equational Theory (Extended Version), J Paykin, S Zdancewic PDF 2019