Time and Location

  • Date: Friday, October 18
  • Time: 2:00-3:00 PM
  • Location: Luddy Hall 4063

Abstract

This is the first in a series of lectures introducing how the language of category theory captures “dependency.” 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.