This is to say that (length-indexed) "Arrays" are Representable functors[1]. A `Vec n a` is isomorphic to (Fin n -> a), where Fin n = { x :: Nat | x < n }.

  instance pi n. Representable (Vec n) where
    type Rep (Vec n) = Fin n
    index :: Vec n a -> (Fin n -> a)
    index = ..
    tabulate :: (Fin n -> a) -> Vec n a
    tabulate = ..

[1] https://hackage-content.haskell.org/package/adjunctions-4.4....