Voevodsky's Univalence Axiom in homotopy type theory
Steve Awodey, \'Alvaro Pelayo, and Michael A. Warren
TL;DR
This paper introduces homotopy type theory and explains Voevodsky's univalent interpretation, highlighting its role in the univalent foundations program at the intersection of algebraic topology and logic.
Contribution
It provides an overview of homotopy type theory and details Voevodsky's univalence axiom, advancing the foundational framework of mathematics.
Findings
Introduction of homotopy type theory as a new mathematical field
Explanation of Voevodsky's univalence axiom and interpretation
Highlighting the significance of the univalent foundations program
Abstract
In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky's univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.
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.