English
Naturality of traverse with respect to an applicative transformation η between F and G: applying η to a traversed tree equals traversing with η.app composed with the function.
Русский
Естественность перебора относительно апликативного преобразования η между F и G: применение η к перебору дерева равно перебору с композицией η.app ∘ f.
LaTeX
$$$ \forall η:\mathrm{ApplicativeTransformation} F G,\forall f:\alpha \to F \beta,\forall t:\mathrm{Tree}\ \alpha,\ η( t.traverse f ) = t.traverse (η.app \beta \circ f). $$$
Lean4
theorem naturality {F G : Type u → Type*} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
(η : ApplicativeTransformation F G) {β : Type u} (f : α → F β) (t : Tree α) :
η (t.traverse f) = t.traverse (η.app β ∘ f : α → G β) := by
induction t with
| nil => rw [traverse, traverse, η.preserves_pure]
| node v l r hl hr =>
rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr, Function.comp_apply]
