English
For all functors G,H with applicative structure and commuting applicatives, and a function g: α→Gβ and h: β→Hγ, and x: Multiset α, the traversal over the composite application equals the composition of traversals:\n traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (Functor.map (traverse h) (traverse g x)).
Русский
Пусть существуют совместимые аппликативные структуры и функции g,h. Тогда обход по композиции равен композиции обходов:
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
@[simp]
theorem map_comp_coe {α β} (h : α → β) : Functor.map h ∘ ofList = (ofList ∘ Functor.map h : List α → Multiset β) := by
funext; simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]
