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)