Abstract

We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas, 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. 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. Last, we show how the Univalent Foundations enforces a structuralist view of mathematics embodied in the so-called Structure Identity Principle. 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.