  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.
