Commit 2025-04-02 15:28 b5814933

feat(CategoryTheory/Core): functors and natural transformations induced on cores (#23436) Add a constructor for functors Core C ⥤ Core D from functors C ⥤ D. Show that this construction respects composition and identity functors. Add a constructor for natural isomorphisms of functors of this form, and show compatibility of the construction with respect to composition, identities, left/right whiskering, left/right unitors, and associators.