Course pages 2014–15

# Category Theory and Logic

## Lecture slides

- lecture 1 (9 Oct)
- lecture 2 (14 Oct)
- lecture 3 (16 Oct)
- lecture 4 (21 Oct)
- lecture 5 (23 Oct)
- lecture 6 (28 Oct)
- lecture 7 (30 Oct)
- lecture 8 (4 Nov)
- lecture 9 (6 Nov)
- lecture 10 (11 Nov)
- lecture 11 (13 Nov)
- lecture 12 (18 Nov)
- lecture 13 (20 Nov)
- lecture 14 (25 Nov)
- lecture 15 (27 Nov)
- lecture 16 (2 Dec)

## Lecture summaries

**Lecture 1:**Introduction; some history; content of this course. Definition of category. The category of sets and functions. Alternative definitions of category.**Lecture 2:**Commutative diagrams. Examples of categories: posets and monotone functions; monoids and monoid homomorphisms; a poset as a category; a monoid as a category. Definition of isomorphism. Informal notion of a "category-theoretic" property.**Lecture 3:**Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.**Lecture 4:**Binary products and coproducts. I-ary products. Cartesian categories.**Lecture 5:**Algebraic signatures. Terms over an algebraic signature and their interpretation in a cartesian category.**Lecture 6:**Equational Logic and its soundness for structures in a cartesian category. The internal language of a cartesian category. Algebraic theories as categories.**Lecture 7:**Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples.**Lecture 8:**Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed poset.**Lecture 9:**Simply Typed Lambda Calculus (STLC). Alpha equivalence of terms. The typing relation. Semantics of STLC types and terms in a cartesian closed category (ccc).**Lecture 10:**Capture-avoiding substitution for lambda terms. Semantics of substitution in a ccc. Soundness of the ccc semantics for beta-eta equality of lambda terms.**Lecture 11:**The internal language of a ccc. STLC theories as cccs. The Curry-Howard-Lawvere correspondence. Functors. Contravariance.**Lecture 12:**Identity and composition for functors. Size: small categories and locally small categories. The category of small categories. Finite products of categories.**Lecture 13:**Natural transformations. Functor categories. The category of small categories is cartesian closed.**Lecture 14:**Hom functors. Natural isomorphisms. Adjunctions. Examples of adjoint functors.**Lecture 15:**Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property.**Lecture 16:**Dependent types. Dependent product sets and dependent function sets as adjoint functors. Equivalence of categories. Example: the category of I-indexed sets and functions is equivalent to the slice category Set/I.

## Exercise sheets

- Exercise Sheet 1
- Exercise Sheet 2
- Exercise Sheet 3
- Exercise Sheet
4
This was the graded exercise sheet (25% of final course mark), issued on Tuesday 11 November 2014 and with solutions due back on Monday 17 November 2014.

- Exercise Sheet 5
- Exercise Sheet 6

## Additional material

- The classic text on category theory is
Mac Lane, Saunders.

and is definitely worth looking at if you are feeling mathematically mature.*Categories for the Working Mathematician*. Graduate Texts in Mathematics 5, second ed. (Springer, 1988), ISBN 0-387-98403-8. - The Category Theory Seminar is held at 2.15pm on Tuesdays in Room MR5 of the Centre for Mathematical Sciences.
- Julia Goedecke's Category Theory course for the 2013/4 Mathematical Tripos Part III / Masters of Mathematics.
- Category Theory in the nLab.
- The Catsters' Category Theory Videos.