Homotopy Type Theory course (2020)
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)
homotopy.io - Web-based proof assistant for finitely-presented globular n-categories, for arbitrary n. (User Guide) (Code)
Homotopy Type Theory: Univalent Foundations of Mathematics book (Code)
Kevin Buzzard, Imperial College London: "Is HoTT the way to do mathematics?" (2020)
A functional programmer's guide to homotopy type theory (2016)
A Guide for Computing Stable Homotopy Groups (2018)