Date: 1 November 2019
Location: Hempfield High School, Room 213
 Speaker: Emily Riehl, Johns Hopkins University
   Title: Homotopy types as a foundation for mathematics

Abstract: The Curry-Howard correspondence formalizes an analogy
between computer programs and mathematical proofs. This talk will
introduce alternative foundations for mathematics animated by this
analogy. The basic object is called a type, which can be simultaneously
interpreted as something like a set or as something like a mathematical
proposition. Homotopy type theory refers to the recent discovery that a
type can also be interpreted as something like a topological space. We
will discuss the implications of this homotopy theoretic interpretation
for the so-called univalent foundations of mathematics.