The HoTT library: a formalization of homotopy type theory in Coq

Document Details

Document Type
Pub Defense Publication
Publication Date
Jan 16, 2017
Source ID
10.1145/3018610.3018615

Entities

People

  • Andrej Bauer
  • Bas Spitters
  • Jason Gross
  • Matthieu Sozeau
  • Michael Shulman
  • Peter Lefanu Lumsdaine

Organizations

  • Aarhus University
  • Air Force Office of Scientific Research
  • Air Force Research Laboratory
  • European Research Council
  • Institut National de Recherche en Informatique et en Automatique
  • Massachusetts Institute of Technology
  • National Science Foundation
  • Stockholm University
  • University of Ljubljana
  • University of San Diego
  • Villum Foundation