Topics in Logic: Type Theory

80-518/818

Spring 2025

Course information

• Place: BH 150
• Time: TR 3:30-4:50
• Instructor: Steve Awodey
• Office: Baker 135F
• Office Hour: Thursday 2-3, or by appointment
• Email: awodey@andrew

Overview

This course focuses on type theory as a formal system, as well as its functorial semantics using category theory. Emphasis will be on soundness, completeness, and representation theorems for various systems, with respect to topological, realizability, and (pre)sheaf models. The lambda-calculus, for example, is modeled by cartesian closed categories, which can be represented both topologically and using presheaves (''Kripke models''). Locally cartesian closed categories model dependent type theories. These can be strictified using hyperdoctrines, fibrations, and other tools. We shall also consider Martin-L"of type theory, including universes, inductive types, intensional identity types, as well as Homotopy type theory.

Prerequisites

80-413/713 Category Theory, 80-514/814 Categorical Logic, or equivalent.

Topics

• Simple type theory and cartesian closed categories
• Dependent type theory and locally cartesian closed categories
• Topological, realizability, Kripke, and algebraic semantics
• Kripke-Joyal forcing
• Martin-L"of type theory
• Homotopy type theory

Texts

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

• Carlo Angiuli and Daniel Gratzer, Principles of Dependent Type Theory. https://carloangiuli.com/courses/b619-sp24/notes.pdf
• B. Ahrens, P. Lumsdaine, and P. North. Comparing semantic frameworks for dependently-sorted algebraic theories. Dec. 2024. https://arxiv.org/pdf/2412.19946
• Crole, R. L., Categories for Types. Cambridge University Press, Cambridge, 1993.
• M. Hofmann, Syntax and Semantics of Dependent Types, Semantics and Logics of Computation, A. Pitts and P. Dybjer (ed.s), Cambridge University Press, 2009. https://www.cs.uoregon.edu/research/summerschool/summer14/rwh_notes/ssdt.pdf
• M. Hofmann, Extensional concepts in intensional type theory (thesis). https://ncatlab.org/nlab/files/HofmannExtensionalIntensionalTypeTheory.pdf
• Lambek, J. and Scott, P., Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1986.
• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge University Press (forthcoming). https://arxiv.org/abs/2212.11082
• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book

Requirements

Grades will be based on 3 problem sets and, for graduate students, a presentation in class.

Course materials

• Course outline
• Lecture notes
• Problem sets
• Course Zulip

Updates

Watch this space for news and information!

• We're also using the course zulip for announcements and discussion. Let me know if you want to be added.
• The first set of lecture notes are available - they also include a review of Category Theory and some other material.
• the lecture notes for the introduction have been updated.

---

Steve Awodey
awodey@cmu.edu