Publications based on the HoTT library - HoTT/Coq-HoTT GitHub Wiki

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