The HoTT Library: A formalization of homotopy type theory in Coq

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau +1 more
10/14/2016
cs.LOmath.LO

Official code: HoTT/Coq-HoTT (1,405 stars, last commit 2026-10-09).

Abstract

We report on the development of the HoTT library, a formalization 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 interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

View on arXivView PDF

Code Implementations(1)

HoTT/Coq-HoTTOfficial100%

A Coq library for Homotopy Type Theory

1,405205CSS, LuaMar 26, 20111 weeks agoNOASSERTION
homotopy-type-theorytype-theoryunivalent-foundations

Similar Papers

Theorem prover Arend

82% match2026

Experience Implementing a Performant Category-Theory Library in Coq

80% match1 repo1.4k2014

A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory

76% match2 repos502021

Introduction to Univalent Foundations of Mathematics with Agda

75% match1 repo2372019

A homotopy-type-theoretic generalization of neurosymbolic inference

72% match1 repo2026

Boolean Nearest Neighbor Language in the Knowledge Compilation Map

72% match2024

Cite this paper

@article{bauer2016hott,
  title  = {The HoTT Library: A formalization of homotopy type theory in Coq},
  author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Mike Shulman and Matthieu Sozeau and Bas Spitters},
  year   = {2016},
  eprint = {1610.04591},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1610.04591}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1610.04591.svg)](https://codeofpaper.com/paper/1610.04591)

Discussion