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
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.WithExtensionalityfor example and have the*.WithExtensionalitymodules parametrized on Extensionality