survey.md

Survey of HoTT math libraries

topic	hott-agda (Plain Agda)	agda-unimath (Plain Agda)	cubical (Cubical Agda)	1lab (Cubical Agda)	arend (Arend)	coq-hott (Coq)	unimath (Coq)
Algebra → Groups	yes	yes	yes	yes	yes	yes	yes
Algebra → Rings	no	yes	yes	no	yes	yes	yes
Algebra → Modules	no	no	yes	no	no	no	yes
Algebra → Category theory	yes1, yes2	yes	yes	yes	yes	yes	yes
Algebra → Real numbers	no	no	no	no	yes	no	yes
Algebra → Vector spaces	no	no	no	no	no	no	no
Algebra → Algebras	no	no	yes	no	no	no	yes
HITs → pushouts	yes	yes	yes	no	yes	yes	yes
HITs → joins	yes	yes	yes	no	yes	yes	no
HITs → suspensions	yes	yes	yes	yes	yes	yes	no
HITs → smash	yes	no	yes	no	no	yes	no
HITs → circle	yes	yes	yes	yes	yes	yes	yes
HITs → sphere	yes	yes	yes	yes	yes	yes	no
HITs → torus	yes	no	yes	no	yes	yes	no
HITs → Eilenberg-Mac Lane spaces	yes	no	yes	no	no	yes	no
Homotopy → loop spaces	yes	yes	yes	no	yes	yes	no
Homotopy → 3x3 lemma of fibrations	yes	no	yes	no	no	yes	no
Homotopy → Blakers-Massey	yes	no	yes	no	yes	yes	no
Homotopy → Freudenthal	yes	no	yes	no	no	yes	no
Homotopy → Hurewicz	no	no	no	no	no	wip	no
Homotopy → Hopf fibration	yes	no	yes	no	yes	no	no
Homotopy → Seifert–van Kampen	yes	no	no	no	no	no	no
Homotopy → pi_4(S^3)	no	no	yes	no	no	no	no
Cohomology → co/chain complexes	yes	no	yes	no	no	no	yes
Cohomology → Gysin sequence	no	no	yes	no	no	no	no
Cohomology → Mayer-Vietoris sequence	yes	no	yes	no	no	no	no
Cohomology → Spectral sequences1	no	no	no	no	no	no	no
Cohomology → of spheres	yes	no	yes	no	no	no	no
Cohomology → of tori	yes	no	yes	no	no	no	no
Modalities → internal	yes	no	yes	no	yes	yes	no
Modalities → crisp contexts2	yes	yes	yes	yes	no	no	no

Footnotes

1. Previously formalized in Lean 2, but since Lean 2 is deprecated it's not considered, so this is a row full of "no"s. ↩

2. A language feature that supports crisp variables in the context, per cohesion. Confined to Agda (>= 2.6) at the moment, I believe. ↩