Tags:homotopy type theory, univalent foundations and Voevodsky

Abstract:

A consistent thread running through the three decades of Voevodsky's work is the application of the ideas of homotopy theory in new and surprising ways, first to motives, and then to formalization of proofs and the foundations of mathematics. I will present the story of the latter development, focusing on the points of interest to mathematicians.

Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics