Cambridge Lectures on Categorical Logic and Type Theory

Lent Term 2026

Course information

• Place: Gates Building SS03
• Time: Mondays 3-5 pm, 2 Feb - 9 March
• Instructor: Steve Awodey, Royal Society Wolfson Visiting Fellow
• Office: Gates FC08
• Office Hour: by appointment
• Email: sma212@cam.ac.uk

Overview

This series of 6 lectures focused on simple type theory and its functorial semantics. Emphasis will be on soundness, completeness, and representation theorems with respect to (pre)sheaf models. The lambda-calculus is modeled by cartesian closed categories, which can be represented using presheaves (aka "Kripke models"). As a warm-up, we first review the "proof irrelevant" case of propositional calculus and its Kripke semantics. The completeness theorem is proven via an elegant representation theorem for Heyting algebras due to Joyal, which generalizes the Stone representation theorem for Boolean algebras. In the second half of the series we then consider Kripke semantics and completeness for the simply-typed lambda-calculus.

Prerequisites

A basic course in Category Theory or Type Theory.

Outline

• Part I: Kripke Semantics for Intuitionistic Propositional Calculus

  1. IPC and Heyting algebras
  2. Stone duality and Kripke semantics
  3. Joyal’s embedding theorem

• Part II: Kripke Semantics for Simply Typed Lambda Calculus

  1. STT and CCCs
  2. Kripke semantics for STT
  3. Embedding and completeness theorems

Texts

Lectures are based on a textbook in progress on Categorical Logic and Type Theory, a draft of which will be made available.

The following are recommended for further reading.

• Johnstone, P.T., Stone Spaces, Cambridge University Press, 1982.
• Crole, R. L., Categories for Types. Cambridge University Press, 1993.
• Lambek, J. and Scott, P., Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1986.

Course materials

• Lecture notes

Updates

Watch this space for news and information!

• Here is a first set of lecture notes for Background; they include a review of Category Theory and some other material.
• Here are the lecture notes for Part I.
• Here are the slides from Lecture I.A.

---

Steve Awodey
awodey@cmu.edu