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