Abstract: I will give an introduction to the Univalent Foundations, a new approach to foundations of mathematics, proposed by Voevodsky based on ideas from homotopy theory. The Univalent Foundations are meant to more closely (than set theory) reflect our intuitions about mathematical objects, while also making computer-aided formal verification of proofs essentially straightforward. As an example, I will present the development of category theory in the new foundations (jww Ahrens and Shulman) and will contrast it with that within set theory. I will also discuss possible applications to formal verification of cryptographic standards.