The List functor

I have been reading some notes on Category Theory. One question that is posed is to verify the definition of $\operatorname{List}$ is a functor...

$\operatorname{List}(g \circ f) = (\operatorname{List} g) \circ (\operatorname{List} f)$

I can see this makes sense in programming terms whereby a function $f$ is mapped to a function $\operatorname{map} f$ but how do you prove this in a mathematically rigorous way?

Thanks!

The property in your question is that a functor preserves morphism composition between categories. In functional programming, the map function provides the morphism-mapping part of the List functor. This property can be proved by induction over the structure of the list datatype, using the definition of map.

I'll use Haskell here as its syntax is fairly clean. map is defined:

map :: (a -> b) -> [a] -> [b]
 map f [] = []
 map f (x:xs) = (f x) : (map f xs)

The property we want to prove is:

map (g . f) = (map g) . (map f)

We will proceed by reducing the left-hand side (LHS) and right-hand side (RHS)
of this equation, for the base and inductive cases, and showing them equal.

-
Base case: []

On the LHS:

map (g . f) []
= []                     {map defn. [1st case]}

On the RHS:

((map g) . (map f)) [] 
= (map g) []             {map defn. [1st case], on the right of .}      
= []                     {map defn. [1st case]}

-
Inductive case: x:xs. The inductive hypothesis is that

(map (g . f)) xs = ((map g) . (map f)) xs

On the LHS:

map (g . f) (x:xs)
= ((g . f) x) : (map (g . f) xs)         {map defn. [2nd case]}

On the RHS:

((map g) . (map f)) (x:xs)     
= (map g) ((f x) : (map f xs))            {map defn. [2nd case], on right of .}
= (g (f x)) : (map g (map f xs))          {map defn. [second case]}
= ((g . f) x) : (((map g) . (map f)) xs)  {definition of composition .}
= ((g . f) x) : (map (g . f) xs)          {by inductive hypothesis}

This completes both cases of the inductive proof for the preservation of morphism composition by map for the List functor.

StackExchange Computer Science Q#11488, answer score: 5