|Topic:||Voevodsky's Univalent Foundations for mathematics|
|Affiliation:||University of Illinois at Urbana-Champaign; Visitor, School of Mathematics|
|Date:||Wednesday, January 25|
|Time/Room:||6:00pm - 7:00pm/Dilworth Room|
We'll take a glance at the world of mathematics as viewed through the Univalent Foundations of Voevodsky. In it, "set" and "proposition" are defined in terms of something more fundamental: "type". The formal language fulfills the mathematicians' dream: one cannot even express a property that fails to be invariant under isomorphism. Moreover, it offers the hope that formalization (and thus verification) of today's mathematical knowledge may be accessible.