Andrei Rodin: "Univalent Foundations and Applied Mathematics"

Topos Institute Colloquium, 15th of December 2022.
———
In a series of lectures given in 2003 Vladimir Voevodsky identified two strategic goals for his further mathematical research. The goal number one was to develop a "computerised library of mathematical knowledge". This line of research eventually led Voevodsky to the idea of Univalent Foundations and its implementation with the UniMath library. The goal number two was to "bridge pure and applied mathematics". Voevodsky's research towards the second goal did not bring published results but in an interview given in 2012 he expressed his intention to return to this project in the future and explained a possible role of Univalent Foundations in it.

In this talk based on archival sources I reconstruct Voevodsky’s original strategy of bridging pure and applied mathematics, illustrate it with some examples, and argue that Applied Univalent Foundations is a viable research program.

[1] Andrei Rodin, Voevodsky’s Unfinished Project: Bridging the Gap between Pure and Applied Mathematics, BioSystems, 204 (2021), 104391; preprint arXiv : 2012.01150

[2] UniMath Library : https://github.com/UniMath/UniMath