Till innehåll på sidan

Steve Awodey: Homotopy Type Theory - Lecture series (May 3, 12 and 25)

Tid: Ti 2016-05-03 kl 13.15 - 15.00

Plats: All lectures take place at the Department of Mathematics, Stockholm University, Kräftriket

Medverkande: Steve Awodey (Carnegie Mellon University)

Exportera till kalender

The Topological Actitivies Seminar and the Stockholm Logic Seminar presents a lecture series by Steve Awodey.

Abstract:

This series of three lectures will introduce the basic ideas of this new field of study and indicate some of the current research topics.  Homotopy type theory employs Per Martin-Löf's constructive type theory as a foundation for mathematics in a novel way.  By allowing not only sets but also more general spaces to occur as the basic types of the system, one can reason formally about spaces and mappings up to homotopy equivalence.  New principles of reasoning supporting this homotopy-invariant point of view can be added to the system, while still retaining the machine implementations that underly its practical utility.

(1) The first lecture is intended for a general mathematical audience and provides an overview of homotopy type theory, along with a discussion of the new univalence axiom and the idea of higher inductive types, and a sample of their use in informal and formal reasoning in classical homotopy theory.

(2) The second lecture will develop the connection between HoTT and Quillen model structures, focussing in particular on the cubical model that has recently been the object of much study.

(3) The third lecture will consider an algebraic treatment of type theory based on the theory of polynomial functors and use it to give a solution to the type theoretic coherence problem, concluding with a new cubical model of HoTT.


Schedule

(1) Tuesday, May 3, 13.15-15.00, Room 306, building 6  --- part of the regular Topological Activities Seminar.

(2) Thursday, May 12, 10.00-11.45, Room 37, building 5

(3) Wednesday, May 25, 15.15-17.00, Room 37, building 5

Professor Steve Awodey is one of the leading researchers behind the development of the Homotopy Type Theory programme. His invitation to Stockholm is supported by a grant from the Svante and Maria Arrhenius fund 2015.