A proposition is the (homotopy) type of its proofs
Steve Awodey
TL;DR
This paper introduces homotopy type theory, exploring its foundational role in understanding the structure of proofs as mathematical objects, and surveys its development and significance.
Contribution
It provides an introduction and comprehensive survey of homotopy type theory, highlighting its novel perspective on the nature of proofs and mathematical structures.
Findings
Homotopy type theory offers a new foundation for mathematics.
Proofs can be viewed as mathematical objects within this framework.
The survey emphasizes the significance of homotopy type theory in modern logic.
Abstract
An introduction and survey of homotopy type theory in honor of W.W. Tait.
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
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topics in Algebra · Algebraic Geometry and Number Theory