English
Let G be applicative and commuting. For g: α→Gβ and h: β→γ, and x: Multiset α, we have:\n map (map h) (traverse g x) = traverse (map h ∘ g) x.
Русский
Пусть G аппликативна; для функций g и h и x: Multiset α выполняется равенство: отображение по h после обхода g эквивалентно обходу композиции.
LaTeX
$$$\\mathrm{map}(\\mathrm{map}\\, h)\\big(\\mathrm{traverse}\\ g\\ x\\big) = \\mathrm{traverse}(\\mathrm{map}\\ h \\circ g)\\ x$$$
Lean4
theorem map_traverse {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _} (g : α → G β) (h : β → γ)
(x : Multiset α) : Functor.map (Functor.map h) (traverse g x) = traverse (Functor.map h ∘ g) x :=
by
refine Quotient.inductionOn x ?_
intro
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map]
rw [Traversable.map_traverse']
simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]
