Functors
Review of List in Hask. Functor implementation in Cubical Agda.
Cat: the category of small categories
Contravariant functors
Presheaves: contravariant functors from a category C to Set
Consider the functor from Set⊆ to Set mapping set U to the set of functions U → ℝ, and arrow U ⊆V to the restriction of V → ℝ to U → ℝ. This is the prototypical example of a presheaf. It relates to subtypes in for example Scala.
Monomorphisms and Epimorphisms (we did not get to epimorphims and will cover them next class)
In Set, monic and epic correspond to injective and surjective.
In Mon, monomorphisms are injective functions but epimorphisms are more general;
for example the injection ℕ → ℤ is monic and epic but not a surjection.
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.
Show carefully that Cat is a category.
Define F from Set⊆ to Set mapping set U to the set of functions ℝ → U, and arrow U ⊆V to the restriction of ℝ → U to ℝ → V and prove that F is a covariant functor. Contrast to the presheaf example from lecture.
Given an arrow f : A→ B in Mon, let |f| : |A|→ |B| be the image in Set under the forgetful functor. Prove that if |f| is injective then f is monic and if |f| is surjective then f is epic. Try also to prove the converses of each statement, and note where the difficulty is. In the monic case it can be proved by creating a free monoid from |A| (see Example 2.3 in Awodey), and as shown in class the epic converse does not hold. (We did not cover epimorphisms and the Mon case in class yet, but will do so next time. You can still try doing this exercise based on the reading.)