Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck.
Univalent foundations depart from (although are also compatible with) the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory.
[3][4] A more detailed discussion of the history of some of the ideas that contribute to the current state of univalent foundations can be found at the page on homotopy type theory (HoTT).
A fundamental characteristic of univalent foundations is that they—when combined with the Martin-Löf type theory (MLTT)—provide a practical system for formalization of modern mathematics.
Originally, univalent foundations were devised by Vladimir Voevodsky with the goal of enabling those who work in classical pure mathematics to use computers to verify their theorems and constructions.
[14] An account of the main ideas of univalent foundations and their connection to constructive mathematics can be found in a tutorial by Thierry Coquand.
[a] A presentation of the main ideas from the perspective of classical mathematics can be found in the 2014 review by Alvaro Pelayo and Michael Warren,[17] as well as in the introduction[18] by Daniel Grayson.
The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom[b] and canonicity for natural numbers remains open.
A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[23] with the key remaining issue being the computational property of the eliminator for the identity types.
There are three standard problems whose solution, despite many attempts, could not be constructed using CIC: These unsolved problems indicate that while CIC is a good system for the initial phase of the development of the univalent foundations, moving towards the use of computer proof assistants in the work on its more sophisticated aspects will require the development of a new generation of formal deduction and computation systems.