English
Let η be an applicative transformation between two applicative functors F and G. For any type-alphabet α, β and any vector x of length n with elements in α, and any function f : α → F β, the result of applying η to the traverse of f along x equals the traverse of η ∘ f along x: η(x.traverse f) = x.traverse(η ∘ f).
Русский
Пусть η — приложительная трансформация между двумя аппликативными функторми F и G. Для любой фиксированной размерности вектора n и любого вектора x над α и функции f: α → F β выполняется тождество η(x.traverse f) = x.traverse(η ∘ f).
LaTeX
$$$\\eta\\bigl( x \\mathrm{traverse} f \\bigr) = x \\mathrm{traverse} (\\eta \\circ f) $$$
Lean4
protected theorem naturality {α β : Type u} (f : α → F β) (x : Vector α n) : η (x.traverse f) = x.traverse (@η _ ∘ f) :=
by
induction x with
| nil => simp! [functor_norm, cast, η.preserves_pure]
| cons ih =>
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
rfl
