Commit 2024-06-10 10:34 14973118

View on Github →

chore(Bicategory/Functor): split into two files (#13677) Made a folder Bicategory/Functor and split the file Bicategory/Functor.lean into Bicategory/Functor/Oplax and Bicategory/Functor/Pseudofunctor. This should make it easier to add more code about functors for bicategories.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/Free.lean

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

deleted def CategoryTheory.Pseudofunctor.comp

deleted def CategoryTheory.Pseudofunctor.id

deleted def CategoryTheory.Pseudofunctor.mapFunctor

deleted def CategoryTheory.Pseudofunctor.mkOfOplax

deleted def CategoryTheory.Pseudofunctor.toOplax

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_mapId

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_obj

deleted structure CategoryTheory.Pseudofunctor

Created Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

added def CategoryTheory.Pseudofunctor.comp

added def CategoryTheory.Pseudofunctor.id

added def CategoryTheory.Pseudofunctor.mapFunctor

added def CategoryTheory.Pseudofunctor.mkOfOplax

added def CategoryTheory.Pseudofunctor.toOplax

added theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp

added theorem CategoryTheory.Pseudofunctor.to_oplax_mapId

added theorem CategoryTheory.Pseudofunctor.to_oplax_obj

added structure CategoryTheory.Pseudofunctor

Modified Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean