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.

hoq - Language based on homotopy type theory with an interval.

Homotopy type theory: towards Grothendieck’s dream

Homotopy type theory: A high-level language for invariant mathematics (2019)

Introduction to Homotopy Type Theory

Homotopy type theory in Lean 3

Workshop on Homotopy Type Theory/ Univalent Foundations (2020)