Computer Laboratory

Course pages 2011–12

Category Theory and Logic

Contact.

If you want to discuss the course material or the exercises, just see me at the end of the lecture or send me an email to arrange a time.

Exercise sheets.

The first exercise sheet was handed out Tue Oct 18: [pdf].

The second exercise sheet was handed out Thurs Nov 3: [pdf].

The third exercise sheet was handed out Wed Dec 21: [pdf].

I have also suggested simpler 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, using the resources below. If you 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: Definition of category. Examples: Category of sets; Category of posets; One object category, Empty category.
  • Lecture 2: More examples. Category of monoids; Sierpinski category (two objects and an arrow between them); Arrow category (objects are functions, morphisms are commuting squares).
  • Lecture 3: More on commuting diagrams. Lemma: Pasting two commuting squares together yields a commuting square. Definitions: Terminal object; Isomorphism. Theorem: Terminal objects are unique up-to unique isomorphism. A first look at the definition of a functor.
  • Lecture 4: More on functors. The forgetful functor from monoids to sets. The free monoid on a set. Natural transformations. The arrow category as the category of functors from the Sierpinski category to the category of sets.

Part II. Conjunction, product types and products in categories.

  • Lecture 5: Products and conjunctions. Brief reminder about natural deduction. A simple type theory with products. Judgements inductively defined by rules. Equality of proof terms, inductively defined by rules: reflexivity, symmetry and transitivity; congruence; beta and eta equations.
  • Lecture 6: Interpretation of type theory in set theory. Types are interpreted as sets; Contexts are interpreted as sets; Judgements (terms-in-context) are interpreted as functions between sets. We started moving towards interpretation in different categories. To this end we considered the definition of a product in an arbitrary category, defined as a kind-of universal pair.
  • Lecture 7: Products in categories. Proposition: Finite products = terminal object + binary products. Proof that the category of monoids has binary products: lots of things to check! Interpretation of the type theory in an arbitrary category with products: types are interpreted as objects, and so are contexts; terms are interpreted as morphisms. The interpretation of types is defined by induction on the structure of types. The interpretation of terms is defined by induction on the derivation of judgements.
  • Lecture 8: Soundness of the interpretation of the type theory in a category with products: showing that for any two terms, if their equality is derivable in the type theory then their interprations are equal as morphisms in the category. Completeness: the syntactic category, aka the classifying category, whose objects are types and whose morphisms are equivalence classes of morphisms. Statement that the syntactic category is a free category with finite products.

Part III. Implication, function types, and cartesian closed categories.

  • Lecture 9: The lambda calculus as a term language for function types. Beta and eta laws. Review of interpretation of the lambda calculus in the category of sets. Illustration: Peirce's law is always inhabited in set theory. Further demonstration of Agda.
  • Lecture 10: Towards adjunctions: Cofree objects relative to a functor. Terminal objects, Products, and Exponentials are all instances of this.
  • Lecture 11: More on adjunctions. Three ways of defining "right adjoint": (1) in terms of cofree objects; (2) as a bijection of hom-sets; (3) an algebraic way using natural transformations and two "triangle laws".
  • Lecture 12: Summary of adjunctions. Recap of interpretation of type theory in a cartesian closed category. The main new concept in this lecture was the Yoneda lemma.
  • Lecture 13: Characterization of the function space in the arrow category, using the Yoneda lemma. Proof of the failure of Peirce's law in the arrow category.

Part IV. Predicates, dependent types, monomorphisms and slice categories.

  • Lecture 14: Predicates as functions. Slice categories. Proposition: slice categories always have terminal objects. Definition of pullbacks.
  • Lecture 15: Pullbacks as right adjoints to a diagonal functor. If a category has pullbacks and a terminal object then it has all finite limits (proof omitted). Existential quantification as left adjoint to a pullback functor. Pullbacks capturing the concepts of substitution and weakening.

    Summary Theorem: Let C be a category. The following are equivalent: (1) C has pullbacks; (2) the functor C → [J,C] has a right adjoint (where J is the category * → * ← *); (3) for each morphism f:X→Y, the functor ∑f:C/X→C/Y has a right adjoint.

  • Lecture 16: Monomorphisms. The category Sub(X) which is like the slice category C/X except all the objects must be monomorphisms. In the case where C is the category of sets, the category Sub(X) is equivalent to the poset (P(X),⊆) considered as a category, where P(X) is the powerset of X. This captures the idea of "proof irrelevance" and takes us to more classical model theory. Proposition: monomorphisms are stable under pullback. Thus for each functor f:X→Y, the pullback functor C/Y→ C/X restricts to a functor Sub(Y)→Sub(X). Pullbacks capturing the idea of inverse image of a function.

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: Check that the category of sets satisfies the laws for a category. Check that the composition of two monotone functions is monotone. Check that the one object category satisfies the laws for a category. Something to think about: can you form a category whose objects are types and whose morphisms are well-typed functional programs?
  • Lecture 2: Complete the definition of the category of monoids. Check it satisfies the laws for a category. Explain why a monoid is the same thing as a category with one object. Define composition in the Sierpinski category. Check it satisfies the laws for a category. Complete the definition of the category of arrows.
  • Lecture 3: Complete the definition of the category of arrows. Describe terminal objects in the categories that we have seen so far, and prove that they are indeed terminal objects. Learn the proof of the theorem "terminal objects are unique up-to unique isomorphism"; you should be able to prove it with your eyes shut!
  • Lecture 4: Prove the proposition that says that the monoid of lists is the free monoid. Check that the lists construction yields a functor from the category of sets to the category of monoids. (You can either use the proposition, for a categorical proof, or you can prove it in a concrete way by thinking about lists.) Check that the arrow category can be understood as the category whose objects are functors from the Sierpinski category to the category of sets, and whose morphisms are natural transformations.
  • Lecture 5: Fill in the gaps (1) x:ɑ |- (x,*): ? (2) x:1 |- ? : 1 ⨉ 1 (3) x:ɑ , y:β |- ? : ɑ (4) x:ɑ , y:β⨉γ |- ? : (ɑ⨉β)⨉γ. Try Agda.
  • Lecture 6: Check that the usual product of sets satisfies the universal property of products in categories.
  • Lecture 7: Little things to check when confirming that the category of monoids has products.
  • Lecture 8: Things to check when defining the syntactic category: composition is well-defined, is associative, etc.
  • Lecture 10: Finish checking the details of the product of two categories. Check the details of the cartesian closed structure of the category of sets.
  • Lecture 11: Check the details of the arguments showing that the three ways of defining "adjunction" are equivalent.
  • Lecture 12: Learn a proof of the Yoneda lemma.
  • Lecture 14: Show that the familiar categories (e.g. monoids, posets) have pullbacks.
  • Lecture 16: Complete the proof that, when C is the category of sets, the category Sub(X) is equivalent to the poset (P(X),⊆). Go over the proof that monomorphisms are stable under pullback. Suppose h=g⋅ f; if g and f are monomorphisms, is h? if h and g are monomorphisms, is f? if h and f are monomorphisms, is g? etc

General knowledge

In the lectures I also flag up some general knowledge that you should really know about. If you don't know about it then have a quick browse.

  • Lecture 1: Partially ordered sets.
  • Lecture 2: Powersets. Partial recursive functions.
  • Lecture 3: The following result for set theory: a bijection is the same thing as a function with an inverse.
  • Lecture 6: Structural induction and induction over rule based definitions. See Discrete maths II first year undergraduate course.
  • Lecture 7: Domain theory and cpos. (Not essential for this course but very interesting! See also the undergraduate course.)

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]

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 book 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.