law maybe_map_compose

bend-mathlib@0.8.1.0 · maybe.bend:56

import Base

56# Mapping a composition maps the composition.
57law maybe_map_compose:
58  for ~A: Data
59  for ~B: Data
60  for ~C: Data
61  for -f: A -> B
62  for -g: B -> C
63  for m: Maybe<&2, A>
64  {Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) == Maybe.map(&2, A, C, x => g(f(x)), m) : Maybe<&2, C>}