Univalent Foundations and the Equivalence Principle - Benedikt Ahrens

Explore univalent foundations and the equivalence principle in mathematics through this lecture from the Vladimir Voevodsky Memorial Conference. Delve into the concept of foundations in mathematics, indiscernability of identicals, and Voevodsky's homotopy lambda calculus. Examine type theory, including dependent types and functions, syntax, and inference rules. Investigate the identity type, contractible types, propositions, and sets. Learn about equivalences, path types, and axioms characterizing path types. Discover how the equivalence principle applies to set-level structures and categories. Gain insights into monoids in type theory and monoid isomorphisms. Presented by Benedikt Ahrens from the University of Birmingham, this comprehensive talk offers a deep dive into advanced mathematical concepts and their applications.

Intro
What is a foundation of mathematics?
Outline
Indiscernability of identicals
Violating the equivalence principle
Voevodsky's homotopy lambda calculus
Overview of type theory
Dependent types and functions
Syntax of type theory
Type dependency
Dependent types in pictures
Inference rules and derivations
The singleton type
The type of dependent pairs
The type of dependent functions IL
A dependent function in pictures
The identity type
Some terms that can be defined
Contractible types, propositions and sets
Equivalences
The path type of pairs
Axioms to characterize some path types
Transport along isomorphism
Monoids in type theory
The type of monoids
Monoid isomorphisms
Equivalence principle for set-level structures
EP for categories
Conclusions