Univalent foundations is a new approach to formalization of mathematical knowledge which is proposed to replace the approach based on Zermelo- Fraenkel "set theory" ( ZFC ) . Unlike ZFC-based foundations which have never been intended for practical formalization of large bodies of complex mathematical knowledge the univalent foundations are being developed from the very beginning with a view towards the creation of usable computer verified libraries of mathematics . At the heart of the univalent foundations are two mathematical discoveries - the Grothendieck correspondence between homotopy types and infinity groupoids and the recently discovered connection between constructive type theories and homotopy theory . A library of formalized mathematics based on the univalent approach is currently being developed using "proof assistant" Coq.