law map_map

bend-mathlib@0.8.1.0 · list.bend:211

import Base

211# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.
212law map_map:
213  for ~A: Type
214  for ~B: Type
215  for ~C: Type
216  for ~f: A -> B
217  for ~g: B -> C
218  for xs: List<A>
219  {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List<C>}