Commit 2024-09-23 14:47 9c7175d4
View on Github →feat(CategoryTheory): MonoidalClosed instance on functors to Type (#13710)
This PR defines an instance of MonoidalClosed on C ⥤ Type max w v u where C : Type u with [Category.{v} C], and w is an arbitrary universe. An explicit internal hom functor is constructed, and is proved to be a right adjoint to tensorLeft.