Univalent Foundations and the UniMath Library
Anthony Bordg

TL;DR
This paper introduces the Univalent Foundations of mathematics, discusses the UniMath library implementing these ideas, and explores challenges in developing large-scale formalized mathematical libraries, highlighting links between architecture and mathematics.
Contribution
It provides a concise overview of Univalent Foundations, details the UniMath library, and discusses the conceptual connections between mathematical architecture and formalization.
Findings
The UniMath library successfully implements Univalent Foundations.
Challenges in scaling formalized mathematics are identified.
Links between architectural principles and mathematical structures are explored.
Abstract
We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas, followed by a discussion of the UniMath library of formalized mathematics implementing the ideas of the Univalent Foundations (section 1), and the challenges one faces in attempting to design a large-scale library of formalized mathematics (section 2). This leads us to a general discussion about the links between architecture and mathematics where a meeting of minds is revealed between architects and mathematicians (section 3). On the way our odyssey from the foundations to the "horizon" of mathematics will lead us to meet the mathematicians David Hilbert and Nicolas Bourbaki as well as the architect Christopher Alexander.
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.
