Homotopy theory ​

Introduction to Homotopy Type Theory is great.

Links ​

• 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) (Code)
• Arend Standard Library
• 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 (PDF)
• 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)
• Homotopy Type Theory by Egbert Rijke (2012) (HN)
• Egbert Rijke nLab research
• Agda formalisation of the Introduction to Homotopy Type Theory
• Base library for HoTT in Agda
• Spring School on Homotopy Type Theory (Code)
• Dan Christensen: "Reasoning in an ∞-topos with homotopy type theory" (2021)
• Homotopy Type Theory in Agda
• HN: Homotopy Type Theory (2021)
• Math 721: Homotopy Type Theory Course (2021)
• Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda
• Homotopy Type Theory as an Alternative Foundation to Mathematics (Presentation)
• Homotopy Group Intro (Tweet)
• Univalent Foundations of Mathematics Links
• Foundations - Univalent foundations of mathematics in Coq.
• Learning Material for Univalent Mathematics and the UniMath library
• The HoTT Game (Article)
• Cubical 1lab - Formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory. (Code)
• Homotopy Type Theory Course (Notes)
• HoTTEST Summer School 2022
• Spartan implementation of H.O.T.T.
• HoTT notes
• Introduction to Homotopy Type Theory (LMFI 2022)
• Timeline of “foundational” advances in homotopy theory? (2022) (HN)
• Introduction to Homotopy Type Theory (2022)
• Categories with families in HoTT
• Isabelle/HoTT - Implementation of homotopy type theory in the interactive proof assistant Isabelle. (Paper)
• HoTTEST Summer School 2022 (Code)
• Homotopy Type Theory Exercises for MGS 2023