Univalent foundations and the equivalence principle

Printer-friendly versionPrinter-friendly version

Nom de l'orateur: 

Benedikt Ahrens

Etablissement de l'orateur: 

INRIA/ École des Mines de Nantes

Lieu de l'exposé: 

Salle Eole

Date et heure de l'exposé: 

02/06/2016 - 11:00

Résumé de l'exposé: 

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.


User login