English
Same as 101407, restated for different naming: for all G,H with applicative and commuting structures, and g,h, x, the equality holds:\n traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (Functor.map (traverse h) (traverse g x)).
Русский
Тот же факт для другую формулировку: обход по композиции равен композиции обходов.
LaTeX
$$$\\mathrm{traverse}(\\mathrm{Comp.mk} \\circ \\mathrm{Functor.map}\\ h \\circ g)\\ x = \\mathrm{Comp.mk}\\big(\\mathrm{Functor.map}(\\mathrm{traverse}\\ h)\\big(\\mathrm{traverse}\\ g\\ x\\big)\\big)$$$
Lean4
theorem comp_traverse {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H]
{α β γ : Type _} (g : α → G β) (h : β → H γ) (x : Multiset α) :
traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (Functor.map (traverse h) (traverse g x)) :=
by
refine Quotient.inductionOn x ?_
intro
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, functor_norm]
