Mathematical Conversations

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.