# School of Mathematics

## Univalent foundations and the equivalence principle

Abstract: The "equivalence principle" says that meaningful statements in mathematics should be invariant under the appropriate notion of equivalence of the objects under consideration. In set-theoretic foundations, the EP is not enforced; e.g., the statement "1 ϵ Nat" is not invariant under isomorphism of sets. In univalent foundations, on the other hand, the equivalence principle has been proved for many mathematical structures. In this introductory talk, I give an overview of univalent foundations and the equivalence principle therein.

## Galois, Grothendieck and Voevodsky

## Opening Remarks

## On Voevodsky's univalence principle

Its importance for type theory cannot be overestimated: it is like the "induction principle" for arithmetic.

I will recall the homotopy interpretation of type theory and the notion of univalent fibration.

I will describe the connection between univalence and descent in higher toposes.

## A1-algebraic topology : genesis, youth and beyond

## What do we mean by "equal"

Abstract: In the univalent foundation formalism, equality makes sense only between objects of the same type, and is itself a type. We will explain that this is closer to mathematical practice than the Zermelo-Fraenkel notion of equality is.

## The mathematical work of Vladimir Voevodsky

winner, and a faculty member at the Institute for Advanced Study, until his

sudden and unexpected death in 2017 at the age of 51. He had a special flair

for thinking creatively about ways to incorporate topology and homotopy theory

into other fields of mathematics. In this talk for a general audience, I will

sketch his seminal contributions to two broad areas, algebraic geometry and the