mathlib4
mathlib4 copied to clipboard
chore(Bicategory): restructure oplax modifications
This PR moves Oplax modifications to its own file Modification/Oplax.lean and also moves FunctorBicategory.lean to FunctorBicategory/Oplax.lean. This will improve the file structure for later PRs generalizing these constructions to pseudofunctors.
PR summary 4e5e9467f7
Import changes for modified files
No significant changes to the import graph
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.Bicategory.FunctorBicategory |
-325 |
Mathlib.CategoryTheory.Bicategory.Modification.Oplax |
325 |
Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax |
326 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details about this script.
Thanks!
bors merge