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.

I believe we need to assume the axiom of function extensionality to prove that -> is a functor on Sets, and likely we'll need it to prove other common-in-Haskell functors are indeed functors, for example State.

Do we want these instances requiring extensionality in this library, and if so, where should we put them? I propose Categories.Examples.Functor.Sets.WithExtensionality for example and have the *.WithExtensionality modules parametrized on Extensionality