English
The traverse operation over a composition of maps corresponds to composing travereses: traversing with Comp.mk of maps equals composing traverses.
Русский
Операция обхода по композиции отображений эквивалентна композиции обходов: обход с Comp.mk равен композиции обходов.
LaTeX
$$$ Vector.traverse (Comp.mk \\circ (map f) \\circ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x) $$$
Lean4
@[nolint unusedArguments]
protected theorem comp_traverse (f : β → F γ) (g : α → G β) (x : Vector α n) :
Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x) := by
induction x with
| nil =>
simp! [cast, *, functor_norm]
rfl
| cons ih =>
rw [Vector.traverse_def, ih]
simp [functor_norm, Function.comp_def]
