# Category Theory: July 25

### Covered in Class

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

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.

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.

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.

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.