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.

Author: callesonne

Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean

@@ -177,7 +177,7 @@ instance : Bicategory (Adj B) where
 
 /-- The forget pseudofunctor from `Adj B` to `B`. -/
 @[simps]
-def forget₁ : Pseudofunctor (Adj B) B where
+def forget₁ : Adj B ⥤ᵖ B where
   obj a := a.obj
   map x := x.l
   map₂ α := α.τl

Mathlib/CategoryTheory/Bicategory/Coherence.lean

@@ -18,7 +18,7 @@ The proof is almost the same as the proof of the coherence theorem for monoidal
 has been previously formalized in mathlib, which is based on the proof described by Ilya Beylin
 and Peter Dybjer. The idea is to view a path on a quiver as a normal form of a 1-morphism in the
 free bicategory on the same quiver. A normalization procedure is then described by
-`normalize : Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B))`, which is a
+`normalize : FreeBicategory B ⥤ᵖ (LocallyDiscrete (Paths B))`, which is a
 pseudofunctor from the free bicategory to the locally discrete bicategory on the path category.
 It turns out that this pseudofunctor is locally an equivalence of categories, and the coherence
 theorem follows immediately from this fact.
@@ -178,7 +178,7 @@ theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
 
 /-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/
 def normalize (B : Type u) [Quiver.{v + 1} B] :
-    Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B)) where
+    FreeBicategory B ⥤ᵖ (LocallyDiscrete (Paths B)) where
   obj a := ⟨a⟩
   map f := ⟨normalizeAux nil f⟩
   map₂ η := eqToHom <| Discrete.ext <| normalizeAux_congr nil η
@@ -224,7 +224,7 @@ def inclusionMapCompAux {a b : B} :
 free bicategory.
 -/
 def inclusion (B : Type u) [Quiver.{v + 1} B] :
-    Pseudofunctor (LocallyDiscrete (Paths B)) (FreeBicategory B) :=
+    LocallyDiscrete (Paths B) ⥤ᵖ (FreeBicategory B) :=
   { -- All the conditions for 2-morphisms are trivial thanks to the coherence theorem!
     preinclusion B with
     mapId := fun _ => Iso.refl _

Mathlib/CategoryTheory/Bicategory/Free.lean

@@ -320,7 +320,7 @@ theorem liftHom₂_congr {a b : FreeBicategory B} {f g : a ⟶ b} {η θ : Hom
 `free_bicategory B` to `C`.
 -/
 @[simps]
-def lift : Pseudofunctor (FreeBicategory B) C where
+def lift : FreeBicategory B ⥤ᵖ C where
   obj := F.obj
   map := liftHom F
   mapId _ := Iso.refl _

Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

@@ -21,7 +21,7 @@ open Bicategory
 
 namespace Pseudofunctor
 
-variable {B : Type u} [Bicategory.{w, v} B] (F : Pseudofunctor B Cat.{v', u'})
+variable {B : Type u} [Bicategory.{w, v} B] (F : B ⥤ᵖ Cat.{v', u'})
 
 section naturality
 

Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean

@@ -49,7 +49,7 @@ def pseudofunctorOfIsLocallyDiscrete
     (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
       (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom (by simp) := by
         cat_disch) :
-    Pseudofunctor B C where
+    B ⥤ᵖ C where
   obj := obj
   map := map
   map₂ φ := eqToHom (by
@@ -107,7 +107,7 @@ A functor between two categories `C` and `D` can be lifted to a pseudofunctor be
 corresponding locally discrete bicategories.
 -/
 @[simps! obj map mapId mapComp]
-def Functor.toPseudoFunctor : Pseudofunctor (LocallyDiscrete C) (LocallyDiscrete D) :=
+def Functor.toPseudoFunctor : LocallyDiscrete C ⥤ᵖ (LocallyDiscrete D) :=
   pseudofunctorOfIsLocallyDiscrete
     (fun ⟨X⟩ ↦.mk <| F.obj X) (fun ⟨f⟩ ↦ (F.map f).toLoc)
     (fun ⟨X⟩ ↦ eqToIso (by simp)) (fun f g ↦ eqToIso (by simp))
@@ -136,7 +136,7 @@ If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categ
 be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
 -/
 @[simps! obj map mapId mapComp]
-def Functor.toPseudoFunctor' : Pseudofunctor (LocallyDiscrete I) B :=
+def Functor.toPseudoFunctor' : LocallyDiscrete I ⥤ᵖ B :=
   pseudofunctorOfIsLocallyDiscrete
     (fun ⟨X⟩ ↦ F.obj X) (fun ⟨f⟩ ↦ F.map f)
     (fun ⟨X⟩ ↦ eqToIso (by simp)) (fun f g ↦ eqToIso (by simp))
@@ -171,7 +171,7 @@ def mkPseudofunctor {B₀ C : Type*} [Category B₀] [Bicategory C]
     (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
       (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom (by simp) := by
         cat_disch) :
-    Pseudofunctor (LocallyDiscrete B₀) C :=
+    LocallyDiscrete B₀ ⥤ᵖ C :=
   pseudofunctorOfIsLocallyDiscrete (fun b ↦ obj b.as) (fun f ↦ map f.as)
     (fun _ ↦ mapId _) (fun _ _ ↦ mapComp _ _) (fun _ _ _ ↦ map₂_associator _ _ _)
     (fun _ ↦ map₂_left_unitor _) (fun _ ↦ map₂_right_unitor _)

Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

@@ -34,8 +34,6 @@ namespace CategoryTheory
 
 open Category Bicategory
 
-open Bicategory
-
 universe w₁ w₂ w₃ v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {B : Type u₁} [Bicategory.{w₁, v₁} B] {C : Type u₂} [Bicategory.{w₂, v₂} C]
@@ -79,6 +77,11 @@ structure Pseudofunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u
       map₂ (ρ_ f).hom = (mapComp f (𝟙 b)).hom ≫ map f ◁ (mapId b).hom ≫ (ρ_ (map f)).hom := by
     cat_disch
 
+/-- Notation for a pseudofunctor between bicategories. -/
+-- Given similar precedence as ⥤ (26).
+-- For example, `C × D ⥤ E` should parse as `(C × D) ⥤ E` not `C × (D ⥤ E)`.
+scoped[CategoryTheory.Bicategory] infixr:26 " ⥤ᵖ " => Pseudofunctor -- type as \func\^p
+
 initialize_simps_projections Pseudofunctor (+toPrelaxFunctor, -obj, -map, -map₂)
 
 namespace Pseudofunctor
@@ -102,7 +105,7 @@ attribute [nolint docBlame] CategoryTheory.Pseudofunctor.mapId
   CategoryTheory.Pseudofunctor.map₂_left_unitor
   CategoryTheory.Pseudofunctor.map₂_right_unitor
 
-variable (F : Pseudofunctor B C)
+variable (F : B ⥤ᵖ C)
 
 /-- The oplax functor associated with a pseudofunctor. -/
 @[simps]
@@ -111,7 +114,7 @@ def toOplax : OplaxFunctor B C where
   mapId := fun a => (F.mapId a).hom
   mapComp := fun f g => (F.mapComp f g).hom
 
-instance hasCoeToOplax : Coe (Pseudofunctor B C) (OplaxFunctor B C) :=
+instance hasCoeToOplax : Coe (B ⥤ᵖ C) (OplaxFunctor B C) :=
   ⟨toOplax⟩
 
 /-- The Lax functor associated with a pseudofunctor. -/
@@ -127,22 +130,22 @@ def toLax : LaxFunctor B C where
     rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
     simp
 
-instance hasCoeToLax : Coe (Pseudofunctor B C) (LaxFunctor B C) :=
+instance hasCoeToLax : Coe (B ⥤ᵖ C) (LaxFunctor B C) :=
   ⟨toLax⟩
 
 /-- The identity pseudofunctor. -/
 @[simps]
-def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : Pseudofunctor B B where
+def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : B ⥤ᵖ B where
   toPrelaxFunctor := PrelaxFunctor.id B
   mapId := fun a => Iso.refl (𝟙 a)
   mapComp := fun f g => Iso.refl (f ≫ g)
 
-instance : Inhabited (Pseudofunctor B B) :=
+instance : Inhabited (B ⥤ᵖ B) :=
   ⟨id B⟩
 
 /-- Composition of pseudofunctors. -/
 @[simps]
-def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D where
+def comp (F : B ⥤ᵖ C) (G : C ⥤ᵖ D) : B ⥤ᵖ D where
   toPrelaxFunctor := F.toPrelaxFunctor.comp G.toPrelaxFunctor
   mapId := fun a => G.map₂Iso (F.mapId a) ≪≫ G.mapId (F.obj a)
   mapComp := fun f g => (G.map₂Iso (F.mapComp f g)) ≪≫ G.mapComp (F.map f) (F.map g)
@@ -155,7 +158,7 @@ def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D whe
 
 section
 
-variable (F : Pseudofunctor B C) {a b : B}
+variable (F : B ⥤ᵖ C) {a b : B}
 
 @[to_app (attr := reassoc)]
 lemma mapComp_assoc_right_hom {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
@@ -288,7 +291,7 @@ end
 
 /-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms. -/
 @[simps]
-def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C where
+def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : B ⥤ᵖ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := F'.mapIdIso
   mapComp := F'.mapCompIso
@@ -306,7 +309,7 @@ def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C whe
 /-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms. -/
 @[simps!]
 noncomputable def mkOfOplax' (F : OplaxFunctor B C) [∀ a, IsIso (F.mapId a)]
-    [∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : Pseudofunctor B C where
+    [∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : B ⥤ᵖ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := fun a => asIso (F.mapId a)
   mapComp := fun f g => asIso (F.mapComp f g)
@@ -324,7 +327,7 @@ noncomputable def mkOfOplax' (F : OplaxFunctor B C) [∀ a, IsIso (F.mapId a)]
 
 /-- Construct a pseudofunctor from a lax functor whose `mapId` and `mapComp` are isomorphisms. -/
 @[simps]
-def mkOfLax (F : LaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C where
+def mkOfLax (F : LaxFunctor B C) (F' : F.PseudoCore) : B ⥤ᵖ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := F'.mapIdIso
   mapComp := F'.mapCompIso
@@ -343,7 +346,7 @@ def mkOfLax (F : LaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C where
 /-- Construct a pseudofunctor from a lax functor whose `mapId` and `mapComp` are isomorphisms. -/
 @[simps!]
 noncomputable def mkOfLax' (F : LaxFunctor B C) [∀ a, IsIso (F.mapId a)]
-    [∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : Pseudofunctor B C :=
+    [∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : B ⥤ᵖ C :=
   mkOfLax F
   { mapIdIso := fun a => (asIso (F.mapId a)).symm
     mapCompIso := fun f g => (asIso (F.mapComp f g)).symm }

Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -48,7 +48,7 @@ This is consistent with the convention for the Grothendieck construction on 1-fu
 ## Future work / TODO
 
 1. Once the bicategory of pseudofunctors has been defined, show that this construction forms a
-pseudofunctor from `Pseudofunctor (LocallyDiscrete 𝒮) Catᵒᵖ` to `Cat`.
+pseudofunctor from `LocallyDiscrete 𝒮 ⥤ᵖ Catᵒᵖ` to `Cat`.
 2. Deduce the results in `CategoryTheory.Grothendieck` as a specialization of
    `Pseudofunctor.Grothendieck`.
 3. Dualize all `CoGrothendieck` results to `Grothendieck`.
@@ -70,15 +70,15 @@ variable {𝒮 : Type u₁} [Category.{v₁} 𝒮]
 /-- The type of objects in the fibered category associated to a pseudofunctor from a
 1-category to Cat. -/
 @[ext]
-structure Grothendieck (F : Pseudofunctor (LocallyDiscrete 𝒮) Cat.{v₂, u₂}) where
+structure Grothendieck (F : LocallyDiscrete 𝒮 ⥤ᵖ Cat.{v₂, u₂}) where
   /-- The underlying object in the base category. -/
   base : 𝒮
   /-- The object in the fiber of the base object. -/
   fiber : F.obj ⟨base⟩
 
 namespace Grothendieck
 
-variable {F : Pseudofunctor (LocallyDiscrete 𝒮) Cat.{v₂, u₂}}
+variable {F : LocallyDiscrete 𝒮 ⥤ᵖ Cat.{v₂, u₂}}
 
 /-- Notation for the Grothendieck category associated to a pseudofunctor `F`. -/
 scoped prefix:75 "∫ " => Grothendieck
@@ -111,15 +111,15 @@ end Grothendieck
 /-- The type of objects in the fibered category associated to a contravariant
 pseudofunctor from a 1-category to Cat. -/
 @[ext]
-structure CoGrothendieck (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}) where
+structure CoGrothendieck (F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat.{v₂, u₂}) where
   /-- The underlying object in the base category. -/
   base : 𝒮
   /-- The object in the fiber of the base object. -/
   fiber : F.obj ⟨op base⟩
 
 namespace CoGrothendieck
 
-variable {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}}
+variable {F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat.{v₂, u₂}}
 
 /-- Notation for the CoGrothendieck category associated to a pseudofunctor `F`. -/
 scoped prefix:75 "∫ᶜ " => CoGrothendieck
@@ -190,7 +190,7 @@ variable (F)
 /-- The projection `∫ᶜ F ⥤ 𝒮` given by projecting both objects and homs to the first
 factor. -/
 @[simps]
-def forget (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}) : ∫ᶜ F ⥤ 𝒮 where
+def forget (F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat.{v₂, u₂}) : ∫ᶜ F ⥤ 𝒮 where
   obj X := X.base
   map f := f.base
 
@@ -199,8 +199,8 @@ section
 attribute [local simp]
   Strict.leftUnitor_eqToIso Strict.rightUnitor_eqToIso Strict.associator_eqToIso
 
-variable {F} {G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}}
-  {H : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}}
+variable {F} {G : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat.{v₂, u₂}}
+  {H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat.{v₂, u₂}}
 
 /-- The CoGrothendieck construction is functorial: a strong natural transformation `α : F ⟶ G`
 induces a functor `CoGrothendieck.map : ∫ᶜ F ⥤ ∫ᶜ G`. -/

Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean

@@ -76,7 +76,7 @@ attribute [reassoc (attr := simp)] StrongTrans.naturality_naturality
 
 namespace StrongTrans
 
-variable {F G : Pseudofunctor B C}
+variable {F G : B ⥤ᵖ C}
 
 /-- The underlying oplax transformation of a strong transformation. -/
 @[simps]
@@ -107,17 +107,17 @@ def id : StrongTrans F F where
 instance : Inhabited (StrongTrans F F) :=
   ⟨id F⟩
 
-variable {H : Pseudofunctor B C}
+variable {H : B ⥤ᵖ C}
 
 /-- Vertical composition of strong transformations. -/
 def vcomp (η : StrongTrans F G) (θ : StrongTrans G H) : StrongTrans F H :=
   mkOfOplax (Oplax.StrongTrans.vcomp η.toOplax θ.toOplax)
 
-/-- `CategoryStruct` on `Pseudofunctor B C` where the (1-)morphisms are given by strong
+/-- `CategoryStruct` on `B ⥤ᵖ C` where the (1-)morphisms are given by strong
 transformations. -/
 @[simps! id_app id_naturality_hom id_naturality_inv comp_naturality_hom
 comp_naturality_inv]
-scoped instance categoryStruct : CategoryStruct (Pseudofunctor B C) where
+scoped instance categoryStruct : CategoryStruct (B ⥤ᵖ C) where
   Hom F G := StrongTrans F G
   id F := StrongTrans.id F
   comp := StrongTrans.vcomp

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

@@ -31,7 +31,7 @@ open Bicategory
 namespace Pseudofunctor
 
 variable {B : Type u₁} {C : Type u₂} [Bicategory.{w₁, v₁} B]
-  [Strict B] [Bicategory.{w₂, v₂} C] (F : Pseudofunctor B C)
+  [Strict B] [Bicategory.{w₂, v₂} C] (F : B ⥤ᵖ C)
 
 lemma mapComp'_comp_id {b₀ b₁ : B} (f : b₀ ⟶ b₁) :
     F.mapComp' f (𝟙 b₁) f = (ρ_ _).symm ≪≫ whiskerLeftIso _ (F.mapId b₁).symm := by

Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean

@@ -26,7 +26,7 @@ namespace CategoryTheory.Pseudofunctor.CoGrothendieck
 
 open Functor Opposite Bicategory Fiber
 
-variable {𝒮 : Type*} [Category 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat}
+variable {𝒮 : Type*} [Category 𝒮] {F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat}
 
 section