Commit 2025-07-03 19:53 2731c229
View on Github →chore(CategoryTheory): insert associators and unitors (#26701) Also fixed several wrong associator directions. This PR is extracted from a WIP PR #26601, where the old expressions are type incorrect.
chore(CategoryTheory): insert associators and unitors (#26701) Also fixed several wrong associator directions. This PR is extracted from a WIP PR #26601, where the old expressions are type incorrect.