-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
1 changed file
with
35 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
--- | ||
layout: post | ||
title: "Indexed Families in Category Theory, Part II" | ||
authors: "Carlo Angiuli" | ||
date: 2024-10-25 14:00:00 | ||
categories: Angiuli Fall2024 | ||
--- | ||
|
||
## 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. |