TL;DR
This paper extends free theorems to homotopy type theory, demonstrating that polymorphic functions preserve homotopy groups of higher inductive types, revealing deep connections between type theory and topology.
Contribution
It introduces homotopy-theoretic free theorems derived from the abstraction theorem in homotopy type theory, linking polymorphism with topological invariants.
Findings
Higher inductive types share homotopy groups with certain polymorphic functions
Free theorems in homotopy type theory can be derived from the abstraction theorem
Polymorphic functions preserve homotopical properties of types
Abstract
We show "free theorems" in the style of Wadler for polymorphic functions in homotopy type theory as consequences of the abstraction theorem. As an application, it follows that every space defined as a higher inductive type has the same homotopy groups as some type of polymorphic functions defined without univalence or higher inductive types.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Topology and Set Theory · Homotopy and Cohomology in Algebraic Topology