# Computer Laboratory

Course pages 2013–14

# Category Theory and Logic

### Contact.

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.

### Exercises sheets.

I will hand out exercise sheets as the course goes along.

• Exercise sheet 1: [pdf].
• Exercise sheet 2: [pdf]. Solution: [pdf]
• Exercise sheet 3: [pdf]. Partial solution: [pdf]
• Exercise sheet 4: [pdf].
• Exercise sheet 5 (graded): [pdf].Solution: [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.