This year's Skolem lecture will be given by Professor Steve Awodey of Carnegie Mellon University.

Awodey is participating in the CAS project Homotopy Type Theory and Univalent Forundations.

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.

Organiser:

• Øystein Linnebo