(Continued from September 26, 2012)

The correspondence between homotopy types and higher categorical analogs of groupoids which was first conjectured by Alexander Grothendieck naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure" while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent Foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Martin-Lof type theories.

This lecture was part of the Institute for Advanced Study’s celebration of its eightieth anniversary, and took place during the events related to the Schools of Mathematics and Natural Sciences.