Skolem Lecture 2019: Steve Awodey
The Skolem Lecture is an annual event in honor of the Norwegian mathematician and logician Thoralf Skolem.
This year's Skolem lecture was given by Professor Steve Awodey of Carnegie Mellon University.
Univalence, Invariance, and Intensionality
What does a mathematical proposition mean? Under one standard account, all true mathematical statements mean the same thing, namely True. A more meaningful account is provided by the Propositions-As-Types conception of type theory, according to which the meaning of a proposition is its collection of proofs. The new system of Homotopy Type Theory provides a further refinement: The meaning of a proposition is the homotopy type of its proofs. A homotopy type may be seen as an infinite-dimensional structure, consisting of objects, isomorphisms, isomorphisms of isomorphisms, etc. Such structures represent systems of objects together with all of their higher symmetries. The language of Martin-Löf type theory is an invariant of all such higher symmetries, a fact which is enshrined in the celebrated Principle of Univalence.