Generalize Vec functor further

[Taneb]

I defined Vec′ : ∀ {o} → Bifunctor (Sets o) (Discrete ℕ) (Sets o) but the Discrete ℕ can be generalized to Categories.Category.Instance.Nat.natop taking the right map to be tabulating a new vector by looking up the corresponding element in the old.