Department of Philosophy
Carnegie Mellon University
Pittsburgh, PA  15213

Office: Baker Hall 148

email :

Main page

Category Theory course 80-413/713 (Fall 2020)


Categorical Logic

Spring 2021

Main informations

Zroom for the class

Meeting ID: 943 5020 6924
Accessible from Canvas 80514
Only adresses admitted

Office hours

after each course, in the same zroom, or by appointment


We will be using Piazza for class discussion.


Homework will be available on the Gradescope page of the class.

Slides of the lectures

Other documents


Course description

This course focuses on applications of category theory in logic and computer science. A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a category determined by the theory. This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics. Such categorical models occur, for example, in denotational semantics. e.g. treating the lambda-calculus via the theory of cartesian closed categories. Higher-order logic is treated categorically by the theory of topoi. We shall see how this idea connects logic with topology (the models of a theory form a space).

A prerequisite for this course is familiarity with basic category theory (as treated in the course 80-413/713).

Contact me for any questions, particularly if you are unsure the course is for you.


Course notes of the previous year

Other references:

  • Crole, Categories for Types (CUP, 1994)
    a good reference in connection to computer sciences.
  • Peter Johnstone, Sketches of an Elephant (OSP, 2002)
    Part D is quite a comprehensive reference on 1st order logic (try to read it by discarding all remarks about topoi).
  • Jacob Lurie, course in Categorical logic (MIT, 2018)
    good reference for anyone interested in ultracategories.


  • Homeworks (1/2 of final grade)
  • Presentation (1/2 of final grade)
    • 80-514 : either written or 30'' talk
    • 80-814 : both written and 30'' talk


back to main page


all pictures are copyrighted