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.