Computer Laboratory

Course pages 2012–13

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].
  • Exercise sheet 3: [pdf].
  • Exercise sheet 4: [pdf].

I will also suggest simple exercises during the lectures, which are recalled below.

I will put Agda source files in this directory: [agda].

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.

Part I. Very basic category theory.

  • Lecture 1: Informal discussion about terminal objects. Definition of category. Examples: Category of sets; Category of cpos (for those who have seen cpos before); One object category. Monoids: categories with one object. Some examples of monoids.
  • Lecture 2: The category of monoids. Definition of monoid. Examples: Natural numbers under addition; natural numbers under multiplication; rationals under addition; rationals under multiplication; lists under concatenation; endo-functions under composition. Definition of monoid homomorphism. Examples of monoid homomorphisms. Proposition: Composition of two monoid homomorphisms is a monoid homomorphism. Theorem: Monoids and homomorphisms form a category.
  • Lecture 3: Commuting diagrams. Lemma: commuting diagrams can be pasted together. Definition of category of arrows, whose morphisms are commuting squares. Definition of inverses for morphisms. Definition of isomorphism. Examples of isomorphisms in the category of sets and the category of monoids. Proposition: inverses are unique; proved by pasting together commuting diagrams.
  • Lecture 4: Terminal objects. Definition of terminal object. Examples of terminal objects in various categories including sets, monoids and arrows. Proposition: Terminal objects are unique up to unique isomorphism. We concluded with a discussion about free monoids. Proposition: The monoid of lists of natural numbers is the free monoid on the set of natural numbers.

Part II. Conjunction and Products.

  • Lecture 5: A type theory with products. (No categories in this lecture!) The types are products and unit. The terms are built from pairing, projection, * in the unit type, and variables. We discussed the idea that terms are a concise representation of proofs of propositions. We introduced a theory of equality for terms, built from the laws of equivalence relations, congruence, and beta and eta laws.
  • Lecture 6: Interpretation of the type theory with products inside set theory. (No categories in this lecture!) We interpreted types as sets, contexts as sets, and terms in context as functions between sets. Our interpretation is sound: if two terms in context are provably equal then their interpretations as functions are equal.
  • Lecture 7: Products in categories. Generalized elements. Generalized pairs. Binary products as universal generalized pairs. Examples of binary products in the category of sets, the category of monoids, and the preorder omega. More generally: Products of an indexed family of objects. Instances of this concept include terminal objects, binary products and interpretations of contexts in set theory.
  • Lecture 8: More on products in categories: Products are unique up to unique isomorphism. (All finite products) = (Terminal objects) + (Binary products). Interpretation of type theory in a category with finite products. Soundness theorem: if two terms are provably equal then their interpretations are equal in any category. Demonstration of the product calculus in Agda.
  • Lecture 9: The syntactic category. Objects are types. Morphisms are terms in context modulo provable equality. Composition is substitution. The syntactic category has finite products. Statement of theorem: The syntactic category is a free category with finite products.

Part III. Functors.

  • Lecture 10. Definition of functor and lots of examples. Definition of natural transformation. The arrow category is isomorphic to the category of functors from [the category with two objects and an arrow between them] to the category of sets.
  • Lecture 11. Isomorphism of categories and equivalence of categories. Simple examples of equivalent categories. If a category is equivalent to another one then it has the same universal properties (products, terminal object etc). Universal property of a free category with finite products: mediating morphism is unique up to natural isomorphism. The syntactic category as a free category with finite products. The free category with finite products is unique up to equivalence.
  • Lecture 12. Representability. Definition of a representable functor C(-,c):Cop->Set. A representation for a functor Cop->Set is defined to be a representable functor with a natural isomorphism to it. Examples of a functor Cop->Set for which a representation is a terminal object, and a functor Cop->Set for which a representation is a particular binary product, and a functor Monoid -> Set for which a representation is a free monoid. The Yoneda lemma. We used this to give concise necessary and sufficient conditions for representations.

Part IV. Implication and functions.

  • Lecture 13 Function types. Introduction and elimination: lambda abstraction and function application. Equational laws: equivalence relations, congruence and beta and eta. Demonstration in Agda.
  • Lecture 14 Definition of cartesian closed category in terms of representability. Interpretation of type theory in the category of sets, and more generally in a cartesian closed category. Soundness: any ccc validates the beta and eta laws.
  • Lecture 15 Demonstration that the category of sets is cartesian closed. Demonstration that the category of arrows is cartesian closed. We used the Yoneda lemma to uncover the ccc structure of the category of arrows. We showed that the interpretation of Peirce's law (((A=>B)=>A)=>A) is always inhabited in the category of sets, but not in the category of arrows. Thus Peirce's law is not provable in type theory.

Exercises suggested during lectures.

During the lectures I will suggest some things to go away and check. You should do this asap after the lecture. Unless I say otherwise, the things to check are straightforward and don't require much innovation. I recommend to do these little exercises in detail at first. It's the only way to learn. It will help you to become fluent.

You are always welcome to show me your attempts. That will also help you to understand what I expect in the exam. I am likely to be busy at the end of term so it's best to try to keep up as you go along.

  • Lecture 1: Get familiar with the definition of category. How many categories are there with two objects and three morphisms? Finish defining a category of cpos (if you know what a cpo is). Describe a category whose objects are monoids --- work out what the morphisms should be and describe composition and identities. Given a category C define a category whose objects are triples (X,Y,f) where X and Y are objects of C and f:X->Y.
  • Lecture 2: Complete the proof that the composition of two monoid homomorphisms is a monoid homomorphism.
  • Lecture 3: Finish defining the arrow category.
  • Lecture 4: Finish proving that the free monoid on the natural numbers is the monoid of lists of natural numbers.
  • Lecture 5: Prove weakening and exchange lemmas for the simple type theory.
  • Lecture 6: Prove soundness.
  • Lecture 7: Finish checking that the category of monoids has binary products.
  • Lecture 8: Finish showing that (A*B)*C and A*(B*C) are products of {A,B,C}. Finish showing that the (All finite products) = (Terminal objects) + (Binary products). Finish checking that the interpretation of the product calculus is sound.
  • Lecture 9: Prove basic lemmas about substitution in order to confirm that the syntactic category is indeed a category.
  • Lecture 10: Check all the details involved in making sure that functors compose and that categories and functors form a category. Describe a functor from the category of monoids to the category of categories.
  • Lecture 12: Check that the bijection described in the Yoneda lemma is indeed a bijection. Finish checking that the list monoid is a representation for the given functor Monoid -> Set.
  • Lecture 15: Finish checking that the category of arrows is a cartesian closed category.

Resources.

I often find it helpful to read different books and find out how different people explain things.

Books (all are in the CL library, and you can also look inside at amazon)

  • Conceptual mathematics by FW Lawvere and S Schanuel. This covers a lot of what we will cover, and is at a gentle pace.
  • Category theory by S Awodey. This is a more traditional textbook, and it's very well written.
  • Categories for types by R Crole. This is a nice book that covers what we will cover and it goes beyond.
  • Practical foundations of mathematics by P Taylor. Also available at his webpage.

Online resources

  • nLab, put together by experts in category theory.
  • Wikipedia. Not bad but don't trust it too much.
  • Lecture notes by Barr and Wells [pdf]
  • Lecture notes by Daniele Turi [pdf]

Seminars

More advanced books:

  • Categories for the working mathematician by S Mac Lane. This is considered by many to be the standard textbook on category theory.
  • Higher operads, higher categories by T Leinster. This book will give you an idea about some current advanced topics in category theory. It's quite easy to read. It's also free online at the arxiv.
  • Sheaves in geometry and logic by S Mac Lane and I Moerdijk. This book will give you an idea about advanced applications to geometry and logic.
  • Sketches of an elephant: a topos theory compendium by PT Johnstone. An excellent reference on topos theory.

Programming languages:
  • Agda is the language we will use for exercises. The best way to use it is to load a .agda file inside the Emacs text editor; then the "Agda" menu provide a way of interfacing with Agda. It is installed on the MPhil machines or you can get it here. There is a nice tutorial [pdf] by Ulf Norell, and assorted intros, examples and videos here.
  • Functional programming is a prerequisite for the course. If you haven't tried it before, you could go straight for Agda, or you might prefer to start with a more mainstream langauge, such as ML or Haskell. Paulson's lecture notes for first-year students [pdf] are good.

There are many other resources. Some are better than others. Feel free to ask me about it.