chore(Bicategory/Functor): add notation for lax and oplax functors (#31238)

I am open to suggestion for other notation as well.

Author: callesonne

Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean

@@ -21,7 +21,8 @@ A lax functor `F` between bicategories `B` and `C` consists of
 
 ## Main definitions
 
-* `CategoryTheory.LaxFunctor B C` : an lax functor between bicategories `B` and `C`
+* `CategoryTheory.LaxFunctor B C` : an lax functor between bicategories `B` and `C`, which we
+  denote by `B ⥤ᴸ C`.
 * `CategoryTheory.LaxFunctor.comp F G` : the composition of lax functors
 * `CategoryTheory.LaxFunctor.Pseudocore` : a structure on an Lax functor that promotes a
   Lax functor to a pseudofunctor
@@ -81,6 +82,10 @@ structure LaxFunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u₂)
     ∀ {a b : B} (f : a ⟶ b),
       map₂ (ρ_ f).inv = (ρ_ (map f)).inv ≫ map f ◁ mapId b ≫ mapComp f (𝟙 b) := by cat_disch
 
+/-- Notation for a lax functor between bicategories. -/
+-- Given similar precedence as ⥤ (26).
+scoped[CategoryTheory.Bicategory] infixr:26 " ⥤ᴸ " => LaxFunctor -- type as \func\^L
+
 initialize_simps_projections LaxFunctor (+toPrelaxFunctor, -obj, -map, -map₂)
 
 namespace LaxFunctor
@@ -94,7 +99,7 @@ attribute [simp, reassoc, to_app] map₂_leftUnitor map₂_rightUnitor
 /-- The underlying prelax functor. -/
 add_decl_doc LaxFunctor.toPrelaxFunctor
 
-variable (F : LaxFunctor B C)
+variable (F : B ⥤ᴸ C)
 
 @[reassoc, to_app]
 lemma mapComp_assoc_left {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
@@ -124,12 +129,12 @@ lemma map₂_rightUnitor_hom {a b : B} (f : a ⟶ b) :
 
 /-- The identity lax functor. -/
 @[simps]
-def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : LaxFunctor B B where
+def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : B ⥤ᴸ B where
   toPrelaxFunctor := PrelaxFunctor.id B
   mapId := fun a => 𝟙 (𝟙 a)
   mapComp := fun f g => 𝟙 (f ≫ g)
 
-instance : Inhabited (LaxFunctor B B) :=
+instance : Inhabited (B ⥤ᴸ B) :=
   ⟨id B⟩
 
 /-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
@@ -155,8 +160,8 @@ lemma mapComp'_eq_mapComp {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶
 
 /-- Composition of lax functors. -/
 @[simps]
-def comp {D : Type u₃} [Bicategory.{w₃, v₃} D] (F : LaxFunctor B C) (G : LaxFunctor C D) :
-    LaxFunctor B D where
+def comp {D : Type u₃} [Bicategory.{w₃, v₃} D] (F : B ⥤ᴸ C) (G : C ⥤ᴸ D) :
+    B ⥤ᴸ D where
   toPrelaxFunctor := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
   mapId := fun a => G.mapId (F.obj a) ≫ G.map₂ (F.mapId a)
   mapComp := fun f g => G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)
@@ -187,7 +192,7 @@ def comp {D : Type u₃} [Bicategory.{w₃, v₃} D] (F : LaxFunctor B C) (G : L
 /-- A structure on an Lax functor that promotes an Lax functor to a pseudofunctor.
 
 See `Pseudofunctor.mkOfLax`. -/
-structure PseudoCore (F : LaxFunctor B C) where
+structure PseudoCore (F : B ⥤ᴸ C) where
   /-- The isomorphism giving rise to the lax unity constraint -/
   mapIdIso (a : B) : F.map (𝟙 a) ≅ 𝟙 (F.obj a)
   /-- The isomorphism giving rise to the lax functoriality constraint -/

Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean

@@ -83,7 +83,7 @@ def oplaxFunctorOfIsLocallyDiscrete
     (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
       mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom (by simp) := by
         cat_disch) :
-    OplaxFunctor B C where
+    B ⥤ᵒᵖᴸ C where
   obj := obj
   map := map
   map₂ φ := eqToHom (by
@@ -119,7 +119,7 @@ corresponding locally discrete bicategories.
 This is just an abbreviation of `Functor.toPseudoFunctor.toOplax`.
 -/
 @[simps! obj map mapId mapComp]
-abbrev Functor.toOplaxFunctor : OplaxFunctor (LocallyDiscrete C) (LocallyDiscrete D) :=
+abbrev Functor.toOplaxFunctor : LocallyDiscrete C ⥤ᵒᵖᴸ (LocallyDiscrete D) :=
   F.toPseudoFunctor.toOplax
 
 end
@@ -146,7 +146,7 @@ If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categ
 be promoted to an oplax functor from `LocallyDiscrete I` to `B`.
 -/
 @[simps! obj map mapId mapComp]
-abbrev Functor.toOplaxFunctor' : OplaxFunctor (LocallyDiscrete I) B :=
+abbrev Functor.toOplaxFunctor' : LocallyDiscrete I ⥤ᵒᵖᴸ B :=
   F.toPseudoFunctor'.toOplax
 
 end

Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

@@ -19,7 +19,8 @@ An oplax functor `F` between bicategories `B` and `C` consists of
 
 ## Main definitions
 
-* `CategoryTheory.OplaxFunctor B C` : an oplax functor between bicategories `B` and `C`
+* `CategoryTheory.OplaxFunctor B C` : an oplax functor between bicategories `B` and `C`, which we
+  denote by `B ⥤ᵒᵖᴸ C`.
 * `CategoryTheory.OplaxFunctor.comp F G` : the composition of oplax functors
 
 -/
@@ -81,6 +82,10 @@ structure OplaxFunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u
       map₂ (ρ_ f).hom = mapComp f (𝟙 b) ≫ map f ◁ mapId b ≫ (ρ_ (map f)).hom := by
     cat_disch
 
+/-- Notation for a pseudofunctor between bicategories. -/
+-- Given similar precedence as ⥤ (26).
+scoped[CategoryTheory.Bicategory] infixr:26 " ⥤ᵒᵖᴸ " => OplaxFunctor -- type as \func\op\^L
+
 initialize_simps_projections OplaxFunctor (+toPrelaxFunctor, -obj, -map, -map₂)
 
 namespace OplaxFunctor
@@ -94,7 +99,7 @@ section
 /-- The underlying prelax functor. -/
 add_decl_doc OplaxFunctor.toPrelaxFunctor
 
-variable (F : OplaxFunctor B C)
+variable (F : B ⥤ᵒᵖᴸ C)
 
 @[reassoc, to_app]
 lemma mapComp_assoc_right {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
@@ -127,12 +132,12 @@ theorem mapComp_id_right {a b : B} (f : a ⟶ b) :
 
 /-- The identity oplax functor. -/
 @[simps]
-def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : OplaxFunctor B B where
+def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : B ⥤ᵒᵖᴸ B where
   toPrelaxFunctor := PrelaxFunctor.id B
   mapId := fun a => 𝟙 (𝟙 a)
   mapComp := fun f g => 𝟙 (f ≫ g)
 
-instance : Inhabited (OplaxFunctor B B) :=
+instance : Inhabited (B ⥤ᵒᵖᴸ B) :=
   ⟨id B⟩
 
 /-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
@@ -158,7 +163,7 @@ lemma mapComp'_eq_mapComp {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶
 
 /-- Composition of oplax functors. -/
 --@[simps]
-def comp (F : OplaxFunctor B C) (G : OplaxFunctor C D) : OplaxFunctor B D where
+def comp (F : B ⥤ᵒᵖᴸ C) (G : C ⥤ᵒᵖᴸ D) : B ⥤ᵒᵖᴸ D where
   toPrelaxFunctor := F.toPrelaxFunctor.comp G.toPrelaxFunctor
   mapId := fun a => (G.mapFunctor _ _).map (F.mapId a) ≫ G.mapId (F.obj a)
   mapComp := fun f g => (G.mapFunctor _ _).map (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)
@@ -189,7 +194,7 @@ def comp (F : OplaxFunctor B C) (G : OplaxFunctor C D) : OplaxFunctor B D where
 /-- A structure on an oplax functor that promotes an oplax functor to a pseudofunctor.
 
 See `Pseudofunctor.mkOfOplax`. -/
-structure PseudoCore (F : OplaxFunctor B C) where
+structure PseudoCore (F : B ⥤ᵒᵖᴸ C) where
   /-- The isomorphism giving rise to the oplax unity constraint -/
   mapIdIso (a : B) : F.map (𝟙 a) ≅ 𝟙 (F.obj a)
   /-- The isomorphism giving rise to the oplax functoriality constraint -/

Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

@@ -25,7 +25,8 @@ We provide several constructors for pseudofunctors:
 
 ## Main definitions
 
-* `CategoryTheory.Pseudofunctor B C` : a pseudofunctor between bicategories `B` and `C`
+* `CategoryTheory.Pseudofunctor B C` : a pseudofunctor between bicategories `B` and `C`, which we
+  denote by `B ⥤ᵖ C`.
 * `CategoryTheory.Pseudofunctor.comp F G` : the composition of pseudofunctors
 
 -/
@@ -79,7 +80,6 @@ structure Pseudofunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u
 
 /-- 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₂)
@@ -109,17 +109,17 @@ variable (F : B ⥤ᵖ C)
 
 /-- The oplax functor associated with a pseudofunctor. -/
 @[simps]
-def toOplax : OplaxFunctor B C where
+def toOplax : B ⥤ᵒᵖᴸ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := fun a => (F.mapId a).hom
   mapComp := fun f g => (F.mapComp f g).hom
 
-instance hasCoeToOplax : Coe (B ⥤ᵖ C) (OplaxFunctor B C) :=
+instance hasCoeToOplax : Coe (B ⥤ᵖ C) (B ⥤ᵒᵖᴸ C) :=
   ⟨toOplax⟩
 
 /-- The Lax functor associated with a pseudofunctor. -/
 @[simps]
-def toLax : LaxFunctor B C where
+def toLax : B ⥤ᴸ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := fun a => (F.mapId a).inv
   mapComp := fun f g => (F.mapComp f g).inv
@@ -130,7 +130,7 @@ def toLax : LaxFunctor B C where
     rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
     simp
 
-instance hasCoeToLax : Coe (B ⥤ᵖ C) (LaxFunctor B C) :=
+instance hasCoeToLax : Coe (B ⥤ᵖ C) (B ⥤ᴸ C) :=
   ⟨toLax⟩
 
 /-- The identity pseudofunctor. -/
@@ -291,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) : B ⥤ᵖ C where
+def mkOfOplax (F : B ⥤ᵒᵖᴸ C) (F' : F.PseudoCore) : B ⥤ᵖ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := F'.mapIdIso
   mapComp := F'.mapCompIso
@@ -308,7 +308,7 @@ def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : B ⥤ᵖ C where
 
 /-- 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)]
+noncomputable def mkOfOplax' (F : B ⥤ᵒᵖᴸ C) [∀ a, IsIso (F.mapId a)]
     [∀ {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)
@@ -327,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) : B ⥤ᵖ C where
+def mkOfLax (F : B ⥤ᴸ C) (F' : F.PseudoCore) : B ⥤ᵖ C where
   toPrelaxFunctor := F.toPrelaxFunctor
   mapId := F'.mapIdIso
   mapComp := F'.mapCompIso
@@ -345,7 +345,7 @@ def mkOfLax (F : LaxFunctor B C) (F' : F.PseudoCore) : 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)]
+noncomputable def mkOfLax' (F : B ⥤ᴸ C) [∀ a, IsIso (F.mapId a)]
     [∀ {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

Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean

@@ -52,7 +52,7 @@ variable (B C)
 lax functor `F` from `B` to `C` such that the structure 1-cell
 `𝟙 (obj X) ⟶ map (𝟙 X)` is in fact an identity 1-cell for every `X : B`. -/
 @[kerodon 008R]
-structure StrictlyUnitaryLaxFunctor extends LaxFunctor B C where
+structure StrictlyUnitaryLaxFunctor extends B ⥤ᴸ C where
   map_id (X : B) : map (𝟙 X) = 𝟙 (obj X) := by rfl_cat
   mapId_eq_eqToHom (X : B) : (mapId X) = eqToHom (map_id X).symm := by cat_disch
 

Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean

@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Bicategory.Modification.Oplax
 /-!
 # The bicategory of oplax functors between two bicategories
 
-Given bicategories `B` and `C`, we give a bicategory structure on `OplaxFunctor B C` whose
+Given bicategories `B` and `C`, we give a bicategory structure on `B ⥤ᵒᵖᴸ C` whose
 * objects are oplax functors,
 * 1-morphisms are oplax natural transformations, and
 * 2-morphisms are modifications.
@@ -24,7 +24,7 @@ open scoped Bicategory
 universe w₁ w₂ v₁ v₂ u₁ u₂
 
 variable {B : Type u₁} [Bicategory.{w₁, v₁} B] {C : Type u₂} [Bicategory.{w₂, v₂} C]
-variable {F G H I : OplaxFunctor B C}
+variable {F G H I : B ⥤ᵒᵖᴸ C}
 
 namespace OplaxTrans
 
@@ -65,7 +65,7 @@ variable (B C)
 
 /-- A bicategory structure on the oplax functors between bicategories. -/
 @[simps!]
-scoped instance OplaxFunctor.bicategory : Bicategory (OplaxFunctor B C) where
+scoped instance OplaxFunctor.bicategory : Bicategory (B ⥤ᵒᵖᴸ C) where
   whiskerLeft {_ _ _} η _ _ Γ := whiskerLeft η Γ
   whiskerRight {_ _ _} _ _ Γ η := whiskerRight Γ η
   associator {_ _ _} _ := associator

Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean

@@ -30,9 +30,9 @@ open Category Bicategory
 universe w₁ w₂ v₁ v₂ u₁ u₂
 
 variable {B : Type u₁} [Bicategory.{w₁, v₁} B] {C : Type u₂} [Bicategory.{w₂, v₂} C]
-  {F G : OplaxFunctor B C} (η θ : F ⟶ G)
+  {F G : B ⥤ᵒᵖᴸ C} (η θ : F ⟶ G)
 
-variable {F G : OplaxFunctor B C}
+variable {F G : B ⥤ᵒᵖᴸ C}
 
 /-- A modification `Γ` between oplax natural transformations `η` and `θ` consists of a family of
 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
@@ -92,26 +92,26 @@ end Modification
 
 /-- Category structure on the oplax natural transformations between OplaxFunctors. -/
 @[simps]
-scoped instance category (F G : OplaxFunctor B C) : Category (F ⟶ G) where
+scoped instance category (F G : B ⥤ᵒᵖᴸ C) : Category (F ⟶ G) where
   Hom := Modification
   id := Modification.id
   comp := Modification.vcomp
 
 @[ext]
-lemma ext {F G : OplaxFunctor B C} {α β : F ⟶ G} {m n : α ⟶ β} (w : ∀ b, m.app b = n.app b) :
+lemma ext {F G : B ⥤ᵒᵖᴸ C} {α β : F ⟶ G} {m n : α ⟶ β} (w : ∀ b, m.app b = n.app b) :
     m = n := by
   apply Modification.ext
   ext
   apply w
 
 /-- Version of `Modification.id_app` using category notation -/
 @[simp]
-lemma Modification.id_app' {X : B} {F G : OplaxFunctor B C} (α : F ⟶ G) :
+lemma Modification.id_app' {X : B} {F G : B ⥤ᵒᵖᴸ C} (α : F ⟶ G) :
     Modification.app (𝟙 α) X = 𝟙 (α.app X) := rfl
 
 /-- Version of `Modification.comp_app` using category notation -/
 @[simp]
-lemma Modification.comp_app' {X : B} {F G : OplaxFunctor B C} {α β γ : F ⟶ G}
+lemma Modification.comp_app' {X : B} {F G : B ⥤ᵒᵖᴸ C} {α β γ : F ⟶ G}
     (m : α ⟶ β) (n : β ⟶ γ) : (m ≫ n).app X = m.app X ≫ n.app X :=
   rfl
 

Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

@@ -73,7 +73,7 @@ instance {a : B} : Comonad (𝟙 a) :=
   ComonObj.instTensorUnit (a ⟶ a)
 
 /-- An oplax functor from the trivial bicategory to `B` defines a comonad in `B`. -/
-def ofOplaxFromUnit (F : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B) :
+def ofOplaxFromUnit (F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B) :
     Comonad (F.map (𝟙 ⟨⟨Unit.unit⟩⟩)) where
   comul := F.map₂ (ρ_ _).inv ≫ F.mapComp _ _
   counit := F.mapId _
@@ -91,8 +91,7 @@ def ofOplaxFromUnit (F : OplaxFunctor (LocallyDiscrete (Discrete Unit)) B) :
     rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]
 
 /-- A comonad in `B` defines an oplax functor from the trivial bicategory to `B`. -/
-def toOplax {a : B} (t : a ⟶ a) [Comonad t] :
-    OplaxFunctor (LocallyDiscrete (Discrete Unit)) B where
+def toOplax {a : B} (t : a ⟶ a) [Comonad t] : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B where
   obj _ := a
   map _ := t
   map₂ _ := 𝟙 _
@@ -112,17 +111,17 @@ namespace OplaxTrans
 
 /-- The bicategory of comonads in `B`. -/
 def ComonadBicat (B : Type u) [Bicategory.{w, v} B] :=
-  OplaxFunctor (LocallyDiscrete (Discrete Unit)) B
+  LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
 
 namespace ComonadBicat
 
 open scoped Oplax.OplaxTrans.OplaxFunctor in
 /-- The bicategory of comonads in `B`. -/
 scoped instance : Bicategory (ComonadBicat B) :=
-  inferInstanceAs <| Bicategory (OplaxFunctor (LocallyDiscrete (Discrete PUnit)) B)
+  inferInstanceAs <| Bicategory (LocallyDiscrete (Discrete PUnit) ⥤ᵒᵖᴸ B)
 
 /-- The oplax functor from the trivial bicategory to `B` associated with the comonad. -/
-def toOplax (m : ComonadBicat B) : OplaxFunctor (LocallyDiscrete (Discrete PUnit)) B :=
+def toOplax (m : ComonadBicat B) : LocallyDiscrete (Discrete PUnit) ⥤ᵒᵖᴸ B :=
   m
 
 /-- The object in `B` associated with the comonad. -/