Category Theory: July 25

Covered in Class

1. Categories

   • Untyped lambda calculus

   • Hask. My version of "Hask" has types as objects and total functions between types as morphisms. Hask was originally intended to model Haskell's type system; for problems see for example here.

   • Dual category

2. Functors

   • Definition

   • Basic examples: list in Hask, identity, forgetful. Next week we will define Cat, the category of (small) categories, and look at presheaves.

Suggested Exercises

All exercises are optional; pick any that look interesting and feel free to create your own! I'll be around in the lab on Tuesday from 10-11 and from 12 to about 1:30 if anyone wants to discuss solutions; also I encourage you to work together and discuss the material with each other! Feel free to post also to the #category-theory Slack channel.

See also the exercises in Gilbert Bernstein's Machines, Monoids, Categories handout.

1. Convince yourself that the dual category C^{op} is actually a category: in other words if you take a category and reverse all the arrows, the category laws all hold. This is a good way to review the definition of a category.

2. In class we noted that an example of a functor in the Hask category is the List constructor, where F₀ is List : A → List A and F₁ is map whose signature is (A → B) → (List A → List B) for any types A and B. Prove that the standard definition of map satisfies the functor laws. Is this the only possible definition (given the standard definition of a list) that satisfies the functor laws? Try to either prove this or exhibit a counterexample.

3. For those familiar with dependent types, the standard definition of propositional negation is ¬ P = P → ⊥. Explain why this both makes sense categorically and is exactly the right definition to use to capture negation.