Extensionality?

[Taneb]

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