English
For a fixed length n, the functor sending a type X to the length-n vectors over X, with its type arguments flipped, is traversable. Its traverse and map operations are inherited from the standard Vector constructions.
Русский
Для фиксированной длины n функтор X ↦ Vector X n, после перестановки аргументов, является traversable. Операции обхода и отображения задаются стандартно через векторные конструкторы.
LaTeX
$$$\\mathrm{Traversable}(\\mathrm{flip}\\,\\mathrm{Vector}\\, n)$$$
Lean4
instance : Traversable.{u} (flip Vector n)
where
traverse := @Vector.traverse n
map {α β} := @Vector.map.{u, u} α β n