Cubical Synthetic Homotopy Theory
summary
Claims that computational univalence holds and higher inductive types give genuine computation are backed by a Cubical Agda development that redoes standard homotopy results. Eliminators become interval maps, proofs shrink dramatically (a 3×3 pushout lemma drops from ~2000 to ~200 lines) and the torus proof runs as a ~150‑line construction showing torus ≃ S1 × S1. Attempts to make these constructions compute concrete numeric terms run into Agda reduction and stack limits, so evaluation works in principle but overflows in practice.
AI-written summary · about
chapters (10)
- 0:00Start
- 0:48Explanations about Homotopy Type Theory
- 1:46Homotopy Type Theory Interpretations
- 1:56Universal Injection
- 3:04Motto of Cubicle Type Theory
- 4:22J Eliminator
- 7:32Higher Inductive Types
- 8:34Summary
- 14:57Pattern Matching
- 18:30Conclusion
related talks
40mHigher Inductive Types in Homotopy Type Theory
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
45mA categorical view of computational effects
24mA Computational Interpretation of Compact Closed Categories
56mOn Type-Based Techniques for Program Manipulation
22mA Calculus of Inductive Linear Constructions
53mIntroduction to Intuitionistic Type Theory
11mLocal algebraic effect theories