[Merged by Bors] - chore(CategoryTheory/Action): generalize universes#24547
[Merged by Bors] - chore(CategoryTheory/Action): generalize universes#24547
Conversation
PR summary b824e0a303Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Thanks! bors merge |
Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.
|
Pull request successfully merged into master. Build succeeded: |
Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.
Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.
Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.
Since #21652 the universe restrictions are no longer necessary. This also allows to remove some universe restrictions in the Galois category API.