English
For any applicative transformation η: G→H, and any g: α→Gβ, x: Multiset α, the naturality condition holds: η (traverse g x) = traverse (η ∘ g) x.
Русский
Пусть η — природное преобразование между аппликативными функторными структурами; тогда обход удовлетворяет естественным преобразованиям.
LaTeX
$$$\\eta(\\mathrm{traverse}\\ g\\ x) = \\mathrm{traverse}(\\eta \\circ g)\\ x$$$
Lean4
theorem naturality {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H]
(eta : ApplicativeTransformation G H) {α β : Type _} (f : α → G β) (x : Multiset α) :
eta (traverse f x) = traverse (@eta _ ∘ f) x :=
by
refine Quotient.inductionOn x ?_
intro
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply, ApplicativeTransformation.preserves_map,
LawfulTraversable.naturality]
