Course pages 2013–14
Category Theory and Logic
If you want to discuss the course material or the exercises, just send me an email or see me at the end of the lecture.
I will hand out exercise sheets as the course goes along.
- Exercise sheet 1: [pdf].
- Exercise sheet 4: [pdf].
- Exercise sheet 6: [pdf].
- Exercise sheet 7: [pdf].
I will also suggest simple exercises during the lectures.
Summary of what is lectured.
There are no written notes to accompany this course. If you have to miss a lecture you can try to catch up from my brief summaries. If you really can't work out what was in the lecture, for whatever reason, just send me an email.
- Lecture 1: Motivation: Origin of category theory and relevance of category theory in theoretical computer science. Definition of category. Definition of the category of sets.
- Lecture 2: The category of posets. Examples of finite categories: the empty category, the category with 1 object and 1 morphism, the category with 2 objects and 1 non-identity morphism. Definition of isomorphism. A bijective monotone map that is not an isomorphism in Poset. First universal properties: terminal objects and (binary) products.
- Lecture 3: The category of monoids and monoid homomorphisms. Examples of monoids, examples of monoid homomorphisms. Subcategories. The free monoid on a set A as initial object in the category A/Mon.
- Lecture 4: Monoids and posets as degenerate categories. Functors, forgetful functors U: Mon -> Set, U: Preord -> Set, discrete and codiscrete preorder functors Delta, Nabla : Set -> Preord. Natural transformations.
- Lecture 5: Simply typed lambda calculus with pairs. Natural deduction for the (conjunction, truth, implication)-fragment of constructive propositional logic. The `Curry-Howard "isomorphism"'. An equational theory on simply typed lambda terms with beta rules, eta rules, congruence rules.
- Lecture 6: Binary products. Binary products as terminal objects in a category of spans, target tupeling, cross notation.
- Lecture 7: Finite products. Exponential objects in categories with finite products, exponential objects as terminal objects. Definition of cartesian closed category. Semantics of simply typed lambda calculus in cartesian closed categories: types are interpreted by induction on their structure, using an assignment of objects to type constants. Contexts are interpreted by iterated binary products. Terms are interpreted by induction on their structure.
- Lecture 8: Substitution lemma and soundness theorem for the interpretation of simply typed lambda calculus.
- Lecture 9: Cat as a cartesian closed category. hom-functors. Definition of Yoneda embeddings.
- Lecture 10: Motivation of the concept of adjunctions via free monoids and exponential objects in CCCs. Definition of adjunction. Statement of the criterion for existence of left adjoints.
- Lecture 11: Repetition opposite categories, contravariant functors. First half of the proof of the characterization of the existence of left adjoints.
- Lecture 12: 2nd part of proof of characterization of existence of left adjoints. Characterization of existence of right adjoints. Uniqueness of adjoints. Definition of monad. Monads from adjunctions.
- Lecture 13: Example of a monad: the lifting monad. Intuition about monads in functional programming -- monadic types serve to sequentially accumulate side effects. The Kleisli category of a monad.
- Lecture 14: Presheaves and representable presheaves. Motivation for the Yoneda Lemma: generalize the observation that the singleton mapping of a set into its power set is injective, and that the monotonous map from a preorder into the order of its down-sets that maps each element to the down closure of the corresponding singleton is order reflecting. Definition of faithful functors and full functors. Reminder of the Yoneda embedding. Statement of the Yoneda Lemma.
- Lecture 15: Proof of the Yoneda Lemma. Finite products in functor categories. Application of the Yoneda lemma: exponential objects in presheaf categories.
- Lecture 16: Further topics in categorical logic: quantifiers as adjoints. Hyperdoctrines as categorical models of predicate logic. How to model dependent types using slice categories.