English
Traversing with a composed mapping is compatible with composing traversals, i.e., traversal distributes over composition of maps.
Русский
Перебор через композицию сохраняет совместимость с последовательным применением отображений; перестройка сохраняется при композиции функций.
LaTeX
$$$ t.traverse( (\mathrm{Functor}\.Comp\;\mathrm{mk}) \circ (f \langle \cdot \rangle) \circ g ) = \mathrm{Functor}.Comp\.mk ( (\cdot .\mathrm{traverse} f) \langle (t.traverse g) \rangle ). $$$
Lean4
theorem comp_traverse {F : Type u → Type v} {G : Type v → Type w} [Applicative F] [Applicative G] [LawfulApplicative G]
{β : Type v} {γ : Type u} (f : β → F γ) (g : α → G β) (t : Tree α) :
t.traverse (Functor.Comp.mk ∘ (f <$> ·) ∘ g) = Functor.Comp.mk ((·.traverse f) <$> (t.traverse g)) := by
induction t with
| nil => rw [traverse, traverse, map_pure, traverse]; rfl
| node v l r hl hr =>
rw [traverse, hl, hr, traverse]
simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map, Comp.seq_mk, seq_map_assoc,
map_seq]
rfl
