The Equivalence Principle is an informal principle asserting that equivalent mathematical objects have the same properties. For example, isomorphic groups should have the same group-theoretic properties, and equivalent categories should have the same category-theoretic properties. Vladimir Voevodsky established Univalent Foundations as a foundation of mathematics (based on dependent type theory) in which this principle cannot be violated -- it is a theorem.
In this second talk, I will discuss how we can prove the equivalence principle for certain structures in Univalent Foundations. I will talk about previous work regarding structures like groups and categories. I will also discuss recent work with Ahrens, Shulman, and Tsementzis regarding structures like higher categories.