CATEGORIES, TYPES, LOGICS

Course Description

We will discuss the close connection between category theory and logic. Essentially, certain structured categories have an "internal language," a logical system whose deductions can be interpreted within the structured category in question. Martin-Löf dependent type theory is the internal language of locally cartesian closed categories, and it is the basis of many modern proof assistants and functional programming languages (Lean, Rocq, Agda, etc.). We will learn enough category theory to understand the categorical semantics of Martin-Löf type theory, and use those semantics to prove some syntactic theorems.

This is a student-led colloquium led by Tom Lindquist under the supervision of Stephen Bigelow.