The Future of Homotopy Theory: "I write out of worry about the health of Homotopy Theory as a mathematical discipline that I love"

Homotopy Type Theory Lecture Notes

Course on homotopy theory and type theory, taught jointly with Jaka Smrekar (2019)

Arend - Theorem prover based on Homotopy Type Theory. It natively supports higher inductive types and a version of cubical syntax. (HN)

HoTT and Dependent Types Group by JetBrains

Homotopy Type Theory 2019 (Notes)

HoTT in Idris - Small, incomplete, and inconsistent formalization of homotopy type theory in Idris.