The correspondence between homotopy types and higher categorical analogs of groupoids, 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 Matin-Lof type theories.
We expect that this new approach to the foundations will finally make it practical for mathematicians to use proof development software in their everyday work. The sophistication and user friendliness of such software ("proof assistants") have been growing steadily for decades and its use in computer science is becoming standard. Enabling its use in pure mathematics will be of great benefit to the new generations of mathematicians and to the mathematical community as a whole.
