Commit 2024-10-26 22:53 0fb33467

View on Github →

chore(Bicategory): restructure oplax modifications (#18250) 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.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/CategoryTheory/Bicategory/FunctorBicategory.lean to Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean

Created Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean

added theorem CategoryTheory.Oplax.Modification.comp_app'

added def CategoryTheory.Oplax.Modification.id

added theorem CategoryTheory.Oplax.Modification.id_app'

added def CategoryTheory.Oplax.Modification.vcomp

added theorem CategoryTheory.Oplax.Modification.whiskerLeft_naturality

added theorem CategoryTheory.Oplax.Modification.whiskerRight_naturality

added structure CategoryTheory.Oplax.Modification

added def CategoryTheory.Oplax.ModificationIso.ofComponents

added theorem CategoryTheory.Oplax.ext

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean

deleted theorem CategoryTheory.OplaxNatTrans.Modification.comp_app'

deleted def CategoryTheory.OplaxNatTrans.Modification.id

deleted theorem CategoryTheory.OplaxNatTrans.Modification.id_app'

deleted def CategoryTheory.OplaxNatTrans.Modification.vcomp

deleted theorem CategoryTheory.OplaxNatTrans.Modification.whiskerLeft_naturality

deleted theorem CategoryTheory.OplaxNatTrans.Modification.whiskerRight_naturality

deleted structure CategoryTheory.OplaxNatTrans.Modification

deleted def CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents

deleted theorem CategoryTheory.OplaxNatTrans.ext