Bordg, Anthony (2018) Univalent Foundations and the UniMath Library. [Preprint]
 | There is a more recent version of this item available. |
|
Text
Univalent_Foundations_and_the_UniMath_library.pdf Download (475kB) | Preview |
Abstract
We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas (section 1), followed by a discussion of the large-scale UniMath library of formalized mathematics implementing the ideas of the Univalent Foundations, and the challenges one faces in designing such a library (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). Last, we show how the Univalent Foundations enforces a structuralist view of mathematics embodied in the so-called Structure Identity Principle (section 4). 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 and the philosopher Paul Benacerraf.
| Export/Citation: | EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL |
| Social Networking: |
| Item Type: | Preprint | ||||||
|---|---|---|---|---|---|---|---|
| Creators: |
|
||||||
| Additional Information: | To appear in the Synthese Library series, Springer, volume "Reflections on the Foundations of Mathematics: Set Theory, Univalent Foundations and General Thoughts", Chapter II "What are Homotopy Type Theory and the Univalent Foundations?". | ||||||
| Keywords: | Univalent Foundations, Univalence Axiom, Homotopy Type Theory, UniMath, Benacerraf's Identification Problem, Structure Identity Principle, architecture, formalization of mathematics, proof assistant. | ||||||
| Subjects: | Specific Sciences > Mathematics > Foundations Specific Sciences > Mathematics > Logic Specific Sciences > Mathematics > Practice Specific Sciences > Mathematics > Proof Specific Sciences > Computer Science General Issues > Structure of Theories |
||||||
| Depositing User: | Please delete this account | ||||||
| Date Deposited: | 19 Sep 2018 17:49 | ||||||
| Last Modified: | 19 Sep 2018 17:49 | ||||||
| Item ID: | 15034 | ||||||
| Subjects: | Specific Sciences > Mathematics > Foundations Specific Sciences > Mathematics > Logic Specific Sciences > Mathematics > Practice Specific Sciences > Mathematics > Proof Specific Sciences > Computer Science General Issues > Structure of Theories |
||||||
| Date: | 2018 | ||||||
| URI: | https://philsci-archive.pitt.edu/id/eprint/15034 |
Available Versions of this Item
- Univalent Foundations and the UniMath Library. (deposited 19 Sep 2018 17:49) [Currently Displayed]
Monthly Views for the past 3 years
Monthly Downloads for the past 3 years
Plum Analytics
Actions (login required)
 |
View Item |
![[feed]](http://philsci-archive.pitt.edu/style/images/feed-icon-32x32.png){kind=icon}