Bordg, Anthony (2018) Univalent Foundations and the UniMath Library. The Architecture of Mathematics. [Preprint]

Preview

Text UF_and_UniMath.pdf Download (458kB) | Preview

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.

---

Export/Citation:

EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL

Social Networking:

Share |

---

Item Type:	Preprint
Creators:	Creators Email ORCID Bordg, Anthony bordg.anthony@gmail.com
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, 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:	25 Sep 2018 17:55
Last Modified:	25 Sep 2018 17:55
Item ID:	15057
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/15057

Available Versions of this Item

• Univalent Foundations and the UniMath Library. (deposited 19 Sep 2018 17:49)
  • Univalent Foundations and the UniMath Library. The Architecture of Mathematics. (deposited 24 Sep 2018 16:32)
    • Univalent Foundations and the UniMath Library. The Architecture of Mathematics. (deposited 24 Sep 2018 16:32)
      • Univalent Foundations and the UniMath Library. The Architecture of Mathematics. (deposited 25 Sep 2018 17:55) [Currently Displayed]
        • Univalent Foundations and the UniMath Library. The Architecture of Mathematics. (deposited 18 Nov 2019 16:52)

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item