Univalent foundations and the equivalence principle

Nom de l'orateur
Benedikt Ahrens
Etablissement de l'orateur
INRIA/ École des Mines de Nantes
Date et heure de l'exposé
Lieu de l'exposé
Salle Eole

The "equivalence principle" (EP) says that meaningful statements in mathematics should be invariant under the appropriate notion of equivalence - "sameness" - 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 first give an overview of earlier attempts at designing foundations that satisfy some invariance property. Afterwards I give a brief introduction to the univalent foundations (UF) and present results, both by other and myself, on the validity of EP in UF.