Functor in category theory: The free theorem for fmap

Question

According to nLab article:

https://ncatlab.org/nlab/show/functor

---

Definition

External definition

A functor $F$ from a category $C$ to a category $D$ is a map sending each object $x \in C$ to an object $F(x) \in D$ and each morphism $f : x \to y$ in $C$ to morphism $F(f) : F(x) \to F(y)$ in $D$, such that

• $F$ preserves composition: $F(g\circ f) = F(g)\circ F(f)$ whenever the left-hand side is well-defined,

• $F$ preserves identity morphisms: for each object $x \in C$, $F(1_x) = 1_{F(x)}$.

---

So, functor is often called "structure preserving".

However, there is an interesting article:

https://www.schoolofhaskell.com/user/edwardk/snippets/fmap

---

The free theorem for fmap

When we write down the definition of Functor we carefully state two laws:

1. fmap id = id
2. fmap f . fmap g = fmap (f . g)

These are pretty well known in the Haskell community.

What is less well known is that the second actually follows from the first and parametricity, so you only need to sit down and prove one Functor law when you go to supply a Functor!

This is a “folklore” result, which I've used in conversation many times before, but it continues to surprise folks, so I decided to write up a slow, step by step proof of this result as it is a fun little exercise in equational reasoning.

To prove this we're going to need the free theorem for fmap and a few lemmas.

---

So, my question is does this apply not only to the category of set and function composition but also category theory in general?

Thanks.

Answer 1

Composition following from identity does not hold for the category of sets and functions (to my knowledge), if by that you mean the sets and functions in ZF(C) or the like that mathematicians usually consider. As you mentioned, the given argument relies on parametricity, and the functions definable in set theory needn't be parametric. In fact, assuming that all functions are parametric is anti-classical. Even in constructive scenarios which could admit parametric models, people might want to keep their options open.

It's probably not a huge surprise in light of the above, but things aren't going to work out in a lot of other situations, either. For instance, the argument you referenced is essentially appealing to parametricity to obtain naturality, because parametricity is a stronger requirement than naturality (based on a notion that doesn't involve composition). However, Haskell functions (or those of similar systems) are parametric with respect to a specific sort of "logical relation" that subsumes naturality with respect to a specific category. This parametricity does not automatically imply naturality even with respect to certain related categories. For instance, if you consider functors $\mathsf F, \mathsf G : \mathsf{Type}_M → \mathsf{Type}$ from a Kleisli category, then a parametric function with type $∀ a. \mathsf F(a) → \mathsf G(a)$ is not automatically natural. So, there are examples like this where functoriality doesn't automatically follow just from the identity rule.

For instance, consider the Kleisli category for lists. There is a functor:

$$\mathsf F : \mathsf{Type}_{\mathsf{List}} → \mathsf{Type}$$ $$\mathsf F\ A = \mathsf{List}\ A$$

where the action of $\mathsf F$ on arrows is given by the following code:

-- drops one element of the list unless it has only one element
contract : List A → List A
contract (_ :: xs@(_ :: _)) = xs
contract xs = xs

mapF : (A → List B) → List A → List B
mapF f [] = []
mapF f (x :: xs) = contract (f x) ++ mapF f xs

This action on arrows doesn't satisfy the composition rule, but it does satisfy the identity rule. There is a functorial action for this object mapping (it is the 'bind' operation), but mapF is another function with the same type and behavior on the Kleisli identity arrow (pure or return in Haskell).

I would imagine that composition following from identity is the exception rather than the rule.