Martin-Lof

• Homotopy Type Theory: The Univalence Axiom, Higher Inductive Types, and ∞-Groupoids · 2021-08-11

  A deep dive into the univalent foundations of mathematics, where equality is homotopy, types are spaces, and the universe mirrors the ∞-groupoid of all ∞-groupoids.