Speaker
Emily Riehl
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 (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.
Suggested Reading
Attendees might enjoy googling “path induction” in advance because it feels like magic upon first acquaintance, but this isn’t necessary.