Steve Awodey

Steve Awodey's GitHub pages

View My GitHub Profile

Categorical Logic


Spring 2024

Course information


This course focuses on applications of category theory to logic. A leading idea is functorial semantics, according to which a model of a logical theory is a (set-valued) functor on a structured category representing the theory.
This introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics.
The lambda-calculus, for example, is treated via cartesian closed categories.
Equational theories are represented by categories with finite products, following Lawvere. Hyperdoctrines are used to model first- and higher-order logics, leading to the categorical notion of a topos. Using sheaves, topos theory also subsumes Kripke semantics for modal and intuitionistic logics. And locally cartesian closed categories provide semantics for dependent type theories. Time permitting, we may also consider Martin-L"of type theory and its recent extension to Homotopy type theory.


80-413/713 Category Theory or equivalent.



Course notes will be provided. The following are recommended for further reading.



Grades will be based on 4 problem sets and, for graduate students, a presentation in class with a brief written report.

Course materials


Watch this space for news and information!

Steve Awodey