Time and Location

  • Date: Friday, October 25
  • Time: 2:00-3:00 PM
  • Location: Luddy Hall 4111

Abstract

This is the second in a series of lectures introducing how the language of category theory captures “dependency.” In this lecture, we will discuss slice categories and their structure. (The previous lecture was mostly devoted to background and examples, so you can still catch up if you missed last week.)

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.