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 third talk, I will discuss recent work with Ahrens, Shulman, and Tsementzis in which we build a framework to prove the equivalence principle for higher categorical structures. Our work encompasses bicategories, dagger categories, opetopic categories, and more.