Univalent Foundations of Mathematics

INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS
Topic:Univalent Foundations of Mathematics
Speaker:Vladimir Voevodsky
Affiliation:Professor, School of Mathematics
Date:Friday, December 10
Time/Room:11:00am - 12:00pm/S-101
Video Link:https://video.ias.edu/univalent/voevodsky

The correspondence between homotopy types and higher categorical analogs of groupoids which was 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 Martin-Lof type theories. In this talk I will explain how to define usual mathematical objects starting with homotopy types instead of sets and show how to use Coq to reason about homotopy types.