Time and Location

  • Date: Friday, November 1
  • Time: 2:00-3:00 PM
  • Location: Luddy Hall 4111

Abstract

This is the third in a series of lectures introducing how the language of category theory captures “dependency.” In this lecture, we will continue our discussion of pullbacks, analyzing their relationship to fibers and base change.

In this lecture series we will start with set-indexed families of sets, generalize from Set to arbitrary categories, and conclude with category-indexed families of categories. Topics covered will include bundles and sections, slice categories, pullbacks, base change, and Grothendieck fibrations.

The categorical prerequisites are minimal: I will assume you know about categories, functors, terminal objects, and binary products. Knowledge of dependent type theory is not necessary but may provide additional motivation. If you already know what a Grothendieck fibration is, you probably won’t learn anything new.

By the end of this series, you will be prepared to understand the categorical semantics of dependent type theory (such as comprehension categories, display map categories, and categories with families / natural models), the categorical gluing approach to logical relations, and why everyone loves pullbacks so much.