Prerequisites and abstracts
Mini-courses
Peter Lumsdaine "Univalent Foundations"
Charles Rezk "Higher Topos Theory"
Lectures
Emily Riehl "Towards a 2-topos of ∞-categories"
While the category of large categories is not a topos, Lawvere observed that it does possess a topos-like property, with the category of small sets playing a role analogous to the subobject classifier. In this talk, we'll explain how a 2-topos structure, as axiomatized by Weber and Street, can be deployed to develop the formal category theory of categories. We then describe joint work in progress with Dominic Verity to establish an analogous (∞,2)-topos structure on the 2-category of (∞,1)-categories, that can be deployed to develop a model-independent theory of (∞,1)-categories.
Benedikt Ahrens "Mechanized mathematics in univalent foundations"
The idea of using computers to mechanically check the correctness of mathematical proofs is as old as computers themselves. Today, there is a wide range of `interactive computer proof assistants' - computer programs that assist, to some extent, in writing proofs in a well-specified format. The proofs can then be checked mechanically by the program. Type theories, such as Coquand's Calculus of Constructions, underlie many of today's popular computer proof assistants.
While developing his model of Martin-Löf type theory in simplicial sets, Voevodsky simultaneously started the creation of a library of mechanically checked mathematics in the univalent style, on top of the proof assistant Coq. This library, called "Foundations" by Voevodsky, is today at the core of the "UniMath" library of mechanically checked mathematics, with over 30 contributors and about 175,000 lines of code.
In this lecture, I will give an introduction to, and overview of, the UniMath project: (i) its underlying formal system, (ii) its implementation using the proof assistant Coq, and (iii) the library of mathematics mechanized in this formal system.
André Joyal "Problems and conjectures on polynomial functors and monads in ∞-toposes"
The theory of polynomial functors and monads has applications to type theory and to the theory of operads. The theory was recently extended to polynomial functors in the category of spaces by Gepner, Haugseng and Kock. We conjecture that the (infty,2)-category of polynomial functors (in any infty-topos E) is cartesian closed. (extending a result of Fiore, Gambino, Hyland and Wynskel). The evidence depends on ideas from type theory (Awodey, Fiore). We also conjecture that the infty-category of bimodules between polynomial monads (in any infty-topos E) is cartesian closed (extending a result of Gambino and J). The conjectures can be understood in terms of a conjectural 2-algebraic geometry. There is a connection with Goodwillie's calculus.