homotopy-type-theory topic
cat
A formalization of category theory in cubical Agda
bonak
🧊 An indexed construction of semi-simplicial and semi-cubical types
HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Agda
Agda formalisation of the Introduction to Homotopy Type Theory
cooltt
😎TT
Coq-HoTT
A Coq library for Homotopy Type Theory
cubicaltt
Experimental implementation of Cubical Type Theory
agda-unimath
The agda-unimath library