Commit 2025-11-03 17:34 8be8e0b1

View on Github →

chore(Pseudofunctor): add notation of pseudofunctors (#31171) This is starting to become necessary by now. If anyone has issues with the notation or other suggestions I am happy to change. I am leaving similar changes for Lax and Oplax functors for later, they can be addressed if people are happy with this PR.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean

modified def CategoryTheory.Bicategory.Adj.forget₁

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

Modified Mathlib/CategoryTheory/Bicategory/Free.lean

modified def CategoryTheory.FreeBicategory.lift

Modified Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean

modified def CategoryTheory.Functor.toPseudoFunctor'

modified def CategoryTheory.Functor.toPseudoFunctor

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

modified def CategoryTheory.Pseudofunctor.comp

modified def CategoryTheory.Pseudofunctor.id

modified def CategoryTheory.Pseudofunctor.mkOfLax

modified def CategoryTheory.Pseudofunctor.mkOfOplax

Modified Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

modified def CategoryTheory.Pseudofunctor.CoGrothendieck.forget

modified structure CategoryTheory.Pseudofunctor.CoGrothendieck

modified structure CategoryTheory.Pseudofunctor.Grothendieck

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

Modified Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean