Proof that fmap f . fmap g = fmap (f . g) given fmap id = id, and the free theorem for fmap's signature.

fmap.markdown

##Theorem:

Given fmap id = id:

fmap f . fmap g = fmap (f . g)

To prove this we're going to need a few lemmas:

The free theorem for fmap is

free theorem for fmap :: g . h = k . f => $map g . fmap h = fmap k . $map f

where $map is the "natural map" for f.

The natural map has the properties we're looking for, so what we need to do is use the above theorem to prove fmap f = $map f, and borrow them.

To do that we start with

##Lemma 1:

id . f = f . id

##Proof of Lemma 1:

Left as an exercise for the reader, but intuitively id is the unit for (.). In reality it results in an eta-expanded result.

##Lemma 2:

Given fmap id = id, then

fmap f = $map f

###Proof of Lemma 2:

fmap f 
= {- by $map id = id -}
$map id . fmap f
= {- by free theorem, Lemma 1 as the precondition -} 
fmap id . $map f
= {- by fmap id = id -}
$map f

Now we know that fmap f = $map f pointwise, and if we assume functional extensionality, we can even show fmap = $map.

##Lemma 3:

f . g = (f . g) . id

###Proof of Lemma 3:

Naively, id is the unit for (.). In reality it results in it eta-expanded.

###Proof of Theorem:

We can read this off of the properties of the free theorem several ways.

The easiest one which does not use the same shaped property on $map is to just play with $map id = id

fmap f . fmap g 
= {- by lemma 2, fmap f = $map f -}
$map f . fmap g
= {- by the free theorem for fmap using lemma 3 for the precondition -}
fmap (f . g) . $map id
= {- by $map id = id -}
fmap (f . g)

QED