Add to ORKGWe 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 ...