Steve Awodey's GitHub pages

- Place: BH 150
- Time: TR 3-4:30
- Instructor: Steve Awodey
- Office: Baker 135F
- Office Hour: Tuesday 2-3, or by appointment
- Email: awodey@andrew
- Canvas: https://canvas.cmu.edu/courses/28133
- Zulip: https://baker.hott.dev/#narrow/stream/31-Categorical-Logic
- Zoom meeting id: 948 0306 2750 (
*the passcode is on Canvas or Zulip*)

This course focuses on applications of category theory in 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 determined by the theory. This gives rise to a syntax-invariant notion of a logical theory and 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. Similarly higher-order logic is modelled by the categorical notion of a topos. Using sheaves, topos theory subsumes Kripke semantics for modal and intuitionistic logics. And locally cartesian closed categories provide semantics for dependent type theories. Time permitting, we may consider Martin-L"of type theory and its recent extension to Homotopy type theory.

80-413/713 Category Theory or equivalent.

- Functorial semantics for algebraic theories
- Functorial semantics for elementary logic
- Higher-order logic and basic topos theory
- Sheaf semantics and Grothendieck toposes
- Simple type theory and cartesian closed categories
- Dependent type theory and locally cartesian closed categories
- Homotopy type theory

- Steve Awodey, Category Theory, 2nd edition, Oxford University Press, 2010.
- Crole, R. L.: Categories for Types. Cambridge University Press, Cambridge, 1993.
- Lambek, J. and Scott, P.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, 1986.
- Mac Lane, S. and Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992.

- Asperti, A. and Longo, G.: Categories, Types, and Structures. MIT Press, 1991.
- Barr, M. and Wells, C.: Categories for Computing Science, 3rd edition.
- Borceux, F.: Handbook of Categorical Algebra (Encyclopedia of Mathematics and its Applications). Cambridge University Press, 1994.
- Freyd, P. and Scedrov, A.: Categories, Allegories. North-Holland, 1995.
- Johnstone, P.: Sketches of an Elephant. Cambridge University Press.
- Makkai, M. and Reyes, G.: First-Order Categorical Logic. LNM 611, Springer, 1977.
- Mac Lane, S.: Categories for the Working Mathematician. Springer, 1971. (the standard reference)
- McLarty, C.: Elementary Categories, Elementary Toposes. Oxford Logic Guides 21, Oxford University Press, 1992.

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

Watch this space for news and information!

- Have a look at the first set of lecture notes for a
*review of basic category theory*. - Jan 18: Class begins! Meet on zoom for a course overview and some planning.
- Jan 20: Meet on zoom for a review of category theory, as in the lecture notes.
- There is a course zulip for announcements and discussion.
- Posted the first half of the notes on algebraic theories for those who want to work ahead.
- Added a course outline.
- The notes on algebraic theories are now complete.
- The first half of the notes on propositional logic are now online.
- No class on Tuesday, March 15. Your assignment instead is to watch my tutorial on polynomial functors (both lectures), either live or the recording, in the Topos Institute Polynomial Workshop.
- The notes on propositional logic are now complete.
- The first half of the notes on lambda-calculus are now online.
- The third and final problem set is online.
- If you haven't chosen a final topic, talk to me about it soon. Students lectures will be in the last week of the semester, 4/26,28.
- The notes on lambda-calculus are now complete.