[Merged by Bors] - feat(CategoryTheory/Monoidal): add lemmas for the whiskerings#9995
Closed
yuma-mizuno wants to merge 10 commits intomasterfrom ymizuno-whiskering-extracted2
+132-28
Commits
Commits on Jan 25, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Jan 26, 2024
- committed
Commits on Jan 27, 2024
- committed