[Merged by Bors] - feat(CategoryTheory/Enriched): functor categories are enriched#18009
Closed
joelriou wants to merge 32 commits intomasterfrom enriched-category-functor-category
+223-3
Commits
Commits on Oct 21, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=32){kind=avatar}
Commits on Oct 22, 2024
Commits on Oct 24, 2024
Commits on Oct 25, 2024
Commits on Oct 28, 2024
Commits on Oct 29, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed