PhilSci Archive

Univalent Foundations and the UniMath Library. The Architecture of Mathematics.

Bordg, Anthony (2019) Univalent Foundations and the UniMath Library. The Architecture of Mathematics. in Reflections on the Foundations of Mathematics, Synthese Library, 407.

This is the latest version of this item.

[img]
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: Published Article or Volume
Creators:
CreatorsEmailORCID
Bordg, Anthonybordg.anthony@gmail.com
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: Dr. Anthony Bordg
Date Deposited: 18 Nov 2019 16:52
Last Modified: 18 Nov 2019 16:52
Item ID: 16639
Journal or Publication Title: in Reflections on the Foundations of Mathematics, Synthese Library
Publisher: Springer International Publishing
Official URL: https://www.springer.com/gp/book/9783030156541
DOI or Unique Handle: 10.1007/978-3-030-15655-8
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: 2019
Volume: 407
URI: http://philsci-archive.pitt.edu/id/eprint/16639

Available Versions of this Item

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Altmetric.com

Actions (login required)

View Item View Item