Seminar

Arrow induction and the dependent Yoneda lemma

Higher algebraic structures in algebra, topology and geometry

11 January 15:15 - 17:00

Emily Riehl - Johns Hopkins University

This talk aims to convey why I am excited about the potential of some variant homotopy type theory as a foundation for higher category theory. This will be illustrated by a case study involving the Yoneda lemma for (oo,1)-categories. In homotopy type theory, the contractibility of the based path space is expressed by the principle of ""path induction,"" which says that identity types are freely generated by reflexivity terms. By an analogy in which arrows in an (oo,1)-category are thought of as directed paths, there is an analogous principle of ""arrow induction,"" which says that hom types are freely generated by identity arrows. We explain how this unravels to a ""dependent"" generalization of the Yoneda lemma.

This involves joint work with Dominic Verity and Mike Shulman.

Click here to watch the seminar (Part 2)

Organizers
Gregory Arone
Stockholm University
Tilman Bauer
KTH Royal Institute of Technology
Alexander Berglund
Stockholm University
Søren Galatius
University of Copenhagen
Jesper Grodal,
University of Copenhagen
Thomas Kragh
Uppsala University

Program
Contact

Alexander Berglund

alexb@math.su.se

Søren Galatius

galatius@math.ku.dk

Thomas Kragh

thomas.kragh@math.uu.se

Other
information

For practical matters at the Institute, send an e-mail to administration@mittag-leffler.se