- 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
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.
80-413/713 Category Theory, 80-514/814 Categorical Logic, or equivalent.
- 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
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
Grades will be based on 3 problem sets and, for graduate students, a presentation in class.
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.
- the lecture notes for the introduction are complete.
- the first set of lecture notes for simple type theory are now available.
- A problem set for Chapter 2 on Simple Type Theory is available.
- the second set of lecture notes for simple type theory are now available.
- Here are some other notes on Kripke completeness of Simple Type Theory.
- Also check out the course notes from Fischbachau for a bigger picture.
- the lecture notes for simple type theory are now complete.
- the first set of lecture notes for dependent type theory are now available.
- the second set of lecture notes for dependent type theory are now available.
- A problem set for Chapter 3 on Dependent Type Theory is available.
- The lecture notes for the first section of Chapter 4 on Homotopy Type Theory are now available.