Introduction to Categorical Logic 23

Info. 14-16 lectures of 90 minutes each. Course period covers the first semester of 2023. Meeting once a week. The lectures will be delivered at the Maths department in the Mittag Leffler room, every Thursday from 13 to 15 o'clock. We start the 12th of January.

Syllabus. (1) Foundational aspects of the Yoneda Embedding. (2) Lawvere theories and Universal Algebra. (3) Sketches and Accessible Categories. (4) Hyperdoctrines. (5) Type Theories. (6) Topoi as spaces, sets and theories.

Description. Categorical logic emerged in the Category Theory community after the impulse of Bill Lawvere and succeeded in providing a crisper, sharper, and authentically foundational point of view on mathematical logic. Because of its versatility, the diversity and richness of perspectives, and the historical dilution in several communities (theoretical computer science, model theory, proof theory), its initial unity has taken off in the last years, and often students are only introduced to some aspects of this elephant. This course presents a unified point of view on the most prominent topics of Categorical Logic. It's a safari in the territories of categorical foundations of mathematics, stressing on the dissolution of their borders.

Exam rules. Two exercise sheets (). Oral interview on the contents of the course.

Oral interview! Oral exams will take place on the 5th of June in Hagagatan. We shall start early in the morning, around 10:00. An oral exam will last between 20 and 40 minutes, and I will ask questions on the entire content of the course. The precise order/schedule of the students can be agreed upon informally. If you are busy on that day or if it is inconvenient for you for any reason, we can arrange a different day. Please contact me.

Animated sketch of an elephant.

Audience and Prerequisites. The course is designed for master and Ph.D. students interested in foundations of mathematics and theoretical computer science in a broad sense. A good knowledge of the language of category theory will be a prerequisite for the audience (the equivalent of the whole (!) book by Riehl in bibliography), yet we will re-discover some of its content from a more foundational perspective.

Tentative structure Material Reference
1. The Yoneda-Cantor embedding.
2. Lawvere theories.
3. Varieties.
4. Finitary monads.
5. The Structure-Semantics duality.
6. Sketches.
7. Accessibility and Presentability.
8. Gabriel-Ulmer duality.
9. Hyperdoctrines.
10. Type Theories as proof relevant hyperdoctrines
11. Type Theories and categories with families
12. Topoi as spaces.
13. Topoi as sets.
14. Topoi as objects.
15. Topoi as theories.
16. Godel-Deligne completeness theorem.

Relevance and Impact. All the topics above have proven to have horizontal applications in Logic and Theoretical computer science. Lawvere theories have offered a concrete way to handle algebraic effects since the work of Plotkin and Moggi, their relation to monads has later impacted the design of modern programming languages like Haskell after Walder. The theory of Accessible Categories is the most used framework for categorical model theory, and its versatility has found applications even in algebraic topology via algebraic factorization systems. Hyperdoctrines perfectly capture first order logic, and their idea has inspired Benabou's treatment of fibrations to later deliver Jacobs' approach to type theories et similia. Finally, topos theory has pervasive ramifications in mathematics, being motivated from plain geometry and allowing to represent geometric theories (which include coherent and thus first order logic).


Comments. The course is very dense, and has no intention of completely cover the bibliography above. Instead, one of its main intents is to introduce the students to this corpus of knowledge, making sure that they reach a sufficient level of independence and maturity.