Univalent foundations

In foundations of mathematics, univalent foundations is an approach to the foundations of constructive mathematics based on the idea that mathematics studies structures on "univalent types" that correspond, under the projection to set-theoretic mathematics, to homotopy types. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by the "categorical" mathematics in the style of Alexander Grothendieck. It departs from the use of predicate logic as the underlying formal deduction system, replacing it, at the moment, by a version of the Martin-Löf type theory. The development of the univalent foundations is closely related with the development of homotopy type theory.

Univalent foundations are compatible with structuralism, if an appropriate (i.e. categorical) notion of mathematical structure is adopted.

The main ideas of the univalent foundations were formulated by Vladimir Voevodsky in 2006/2009. The sole reference for the philosophical connections between the univalent foundations and the earlier ideas are Voevodsky's 2014 Bernays lectures. The name "univalence" is due to Voevodsky. A more detailed discussion of the history of some of the ideas that contribute to the current state of the univalent foundations can be found at the page on homotopy type theory.

A fundamental characteristic of the univalent foundations is that they, when combined with the Martin-Löf type theory, provide a practical system for formalization of modern mathematics. A considerable amount of mathematics has been formalized using this system and modern proof assistants such as Coq and Agda. The first such library called "Foundations" was created by Vladimir Voevodsky in 2010. Now Foundations is a part of a larger development with several authors called UniMath. Foundations also inspired other libraries of formalized mathematics, such as the HoTT Coq library and HoTT Agda library, that developed the univalent ideas in new directions.

...
Wikipedia