Presenter: Emily Riehl [John Hopkins]
Title: Arrow induction and the dependent Yoneda lemma
When: Friday, March 3, 2023, 11:00 a.m.
Where: DERR 333 and ZOOM (Zoom info at bottom of page)
Abstract: 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 (∞,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 (∞,1)-category are thought of as directed paths, there is an analogous princi- ple 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.