English
For the flipped vector functor, there is a lawful traversable structure, with all standard traversal laws holding, including id_traverse, comp_traverse, traverse_eq_map_id, naturality, and map laws.
Русский
Для развёрнутого функторa вектора существует законная структура traversable; выполняются все стандартные законы обхода: id_traverse, comp_traverse, traverse_eq_map_id, естественность и законы отображения.
LaTeX
$$$\\text{LawfulTraversable}(\\mathrm{flip}\\,\\mathrm{Vector})\\;n$$$
Lean4
instance : LawfulTraversable.{u} (flip Vector n)
where
id_traverse := @Vector.id_traverse n
comp_traverse := Vector.comp_traverse
traverse_eq_map_id := @Vector.traverse_eq_map_id n
naturality := Vector.naturality
id_map := by intro _ x; cases x; simp! [(· <$> ·)]
comp_map := by intro _ _ _ _ _ x; cases x; simp! [(· <$> ·)]
map_const := rfl
