Higher Inductive Types in Homotopy Type Theory
summary
Defines higher inductive types as data constructors that also supply paths and higher paths, uses recursion/induction principles to treat spheres, integers, circle and torus as concrete types, and proves the torus is equivalent to the product of two circles (torus ≃ S1 × S1) by building mutual maps and checking composites up to path equalities. Work targets formalization in proof assistants (Coq, Agda, Lean) and succeeds in one-off synthetic homotopy proofs.
AI-written summary · about
chapters (7)
- 0:00Start
- 4:35Four-Color Theorem
- 5:00Kepler Conjecture
- 10:47Constructive Type Theory
- 20:07Homotopic Interpretation
- 23:44The Equivalence between the Torus and the Product of the Two Two Circles
- 27:19Principle of Recursion for Soccer Circle
related talks
25mCubical Synthetic Homotopy Theory
27mCanonicity for Indexed Inductive-Recursive Types
22mA Calculus of Inductive Linear Constructions
36mGoing Higher
53mIntroduction to Intuitionistic Type Theory
51mCategory Theory for the Working Hacker
01h 31mCategory Theory Track by Bartosz Milewski Part 2
02h 24mCategory Theory Track