law maybe_map_compose_sym

bend-mathlib@0.8.1.0 · maybe.bend:269

import Base

269# Mapping a composition maps the composition, reversed to rewrite toward the simple side.
270law maybe_map_compose_sym:
271  for ~A: Data
272  for ~B: Data
273  for ~C: Data
274  for -f: A -> B
275  for -g: B -> C
276  for m: Maybe<&2, A>
277  {Maybe.map(&2, A, C, x => g(f(x)), m) == Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) : Maybe<&2, C>}