Transformations between oplax functors

Just as there are natural transformations between functors, there are transformations between oplax functors. The equality in the naturality condition of a natural transformation gets replaced by a specified 2-morphism. Now, there are three possible types of transformations (between oplax functors):

• Oplax natural transformations;
• Lax natural transformations;
• Strong natural transformations. These differ in the direction (and invertibility) of the 2-morphisms involved in the naturality condition.

Main definitions

• Oplax.OplaxTrans F G: oplax transformations between oplax functors F and G. The naturality condition is given by a 2-morphism F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
• Oplax.StrongTrans F G: Strong transformations between oplax functors F and G.

Using these, we define two CategoryStruct (scoped) instances on OplaxFunctor B C, one in the Oplax.OplaxTrans namespace and one in the Oplax.StrongTrans namespace. The arrows in these CategoryStruct's are given by oplax transformations and strong transformations respectively.

We also provide API for going between oplax transformations and strong transformations:

• Oplax.StrongCore F G: a structure on an oplax transformation between oplax functors that promotes it to a strong transformation.
• Oplax.mkOfOplax η η': given an oplax transformation η such that each component 2-morphism is an isomorphism, mkOfOplax gives the corresponding strong transformation.

TODO

This file could also include lax transformations between oplax functors.

References

• Niles Johnson, Donald Yau, 2-Dimensional Categories

structure CategoryTheory.Oplax.OplaxTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : OplaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

If η is an oplax transformation between F and G, we have a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. We also have a 2-morphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b. These 2-morphisms satisfies the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

• app (a : B) : F.obj a ⟶ G.obj a

  The component 1-morphisms of an oplax transformation.

• naturality {a b : B} (f : a ⟶ b) : CategoryStruct.comp (F.map f) (self.app b) ⟶ CategoryStruct.comp (self.app a) (G.map f)

  The 2-morphisms underlying the oplax naturality constraint.

• naturality_naturality {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g) = CategoryStruct.comp (self.naturality f) (Bicategory.whiskerLeft (self.app a) (G.map₂ η))

  Naturality of the oplax naturality constraint.

• naturality_id (a : B) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)) (Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (Bicategory.rightUnitor (self.app a)).inv)

  Oplax unity.

• naturality_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.naturality (CategoryStruct.comp f g)) (Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.naturality g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.naturality f) (G.map g)) (Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

  Oplax functoriality.

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c} (h : CategoryStruct.comp (self.app a) (CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z) : CategoryStruct.comp (self.naturality (CategoryStruct.comp f g)) (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.naturality g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.naturality f) (G.map g)) (CategoryStruct.comp (Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : F.obj a ⟶ G.obj b} (h : CategoryStruct.comp (self.app a) (G.map g) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (CategoryStruct.comp (self.naturality g) h) = CategoryStruct.comp (self.naturality f) (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a} (h : CategoryStruct.comp (self.app a) (CategoryStruct.id (G.obj a)) ⟶ Z) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)) (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapId a)) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (self.app a)).inv h))

@[deprecated CategoryTheory.Oplax.OplaxTrans (since := "2025-04-23")]

def CategoryTheory.OplaxNatTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : OplaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

Alias of CategoryTheory.Oplax.OplaxTrans.

---

If η is an oplax transformation between F and G, we have a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. We also have a 2-morphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b. These 2-morphisms satisfies the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

Equations

• @CategoryTheory.OplaxNatTrans = @CategoryTheory.Oplax.OplaxTrans

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (Bicategory.whiskerLeft f (θ.naturality h)) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g)) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ H.obj b} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality h)) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g)) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h✝)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (Bicategory.whiskerRight (η.naturality g) h) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (Bicategory.associator (η.app a) (G.map g) h).inv))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality g) h) h✝) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map g) h).inv h✝)))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.comp g h))) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (G.map g) (θ.naturality h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (θ.naturality g) (H.map h))) (Bicategory.whiskerLeft f (Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ H.obj c} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.comp (H.map g) (H.map h))) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.comp g h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (G.map g) (θ.naturality h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (θ.naturality g) (H.map h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom) h✝)))))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.comp f g)) h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.comp f g)) h).hom (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapComp f g) h))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (η.naturality g) h)) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (η.naturality f) (G.map g)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (Bicategory.associator (η.app a) (CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.comp (G.map f) (G.map g)) h) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.comp f g)) h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.comp f g)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapComp f g) h)) h✝)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (η.naturality g) h)) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (η.naturality f) (G.map g)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (CategoryStruct.comp (G.map f) (G.map g)) h).hom h✝))))))))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a))) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) {Z : a' ⟶ H.obj a} (h : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.id (H.obj a))) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv) h))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)) f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') {Z : F.obj a ⟶ a'} (h : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.id (G.obj a)) f) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)) f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f)) h)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (CategoryStruct.comp (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom h)))

def CategoryTheory.Oplax.OplaxTrans.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : OplaxTrans F F

The identity oplax transformation.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Oplax.OplaxTrans.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F : OplaxFunctor B C} : Inhabited (OplaxTrans F F)

Equations

• CategoryTheory.Oplax.OplaxTrans.instInhabited = { default := CategoryTheory.Oplax.OplaxTrans.id F }

def CategoryTheory.Oplax.OplaxTrans.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) : OplaxTrans F H

Vertical composition of oplax transformations.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Oplax.OplaxTrans.instCategoryStructOplaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (OplaxFunctor B C)

CategoryStruct on OplaxFunctor B C where the (1-)morphisms are given by oplax transformations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) (a : B) : (CategoryStruct.comp η θ).app a = CategoryStruct.comp (η.app a) (θ.app a)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (a : B) : (CategoryStruct.id F).app a = CategoryStruct.id (F.obj a)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.id_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {x✝ x✝¹ : B} (f : x✝ ⟶ x✝¹) : (CategoryStruct.id F).naturality f = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (Bicategory.leftUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.comp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) {a b : B} (f : a ⟶ b) : (CategoryStruct.comp η θ).naturality f = CategoryStruct.comp (Bicategory.associator (X✝.map f) (η.app b) (θ.app b)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) (θ.app b)) (CategoryStruct.comp (Bicategory.associator (η.app a) (Y✝.map f) (θ.app b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (Bicategory.associator (η.app a) (θ.app a) (Z✝.map f)).inv)))

structure CategoryTheory.Oplax.StrongTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : OplaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

A strong natural transformation between oplax functors F and G is a natural transformation that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:

• a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B.
• a 2-isomorphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
• These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

• app (a : B) : F.obj a ⟶ G.obj a
• naturality {a b : B} (f : a ⟶ b) : CategoryStruct.comp (F.map f) (self.app b) ≅ CategoryStruct.comp (self.app a) (G.map f)
• naturality_naturality {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g).hom = CategoryStruct.comp (self.naturality f).hom (Bicategory.whiskerLeft (self.app a) (G.map₂ η))
• naturality_id (a : B) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)).hom (Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (Bicategory.rightUnitor (self.app a)).inv)
• naturality_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.naturality (CategoryStruct.comp f g)).hom (Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.naturality g).hom) (CategoryStruct.comp (Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.naturality f).hom (G.map g)) (Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

@[deprecated CategoryTheory.Oplax.StrongTrans (since := "2025-04-23")]

def CategoryTheory.Oplax.StrongOplaxNatTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : OplaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

Alias of CategoryTheory.Oplax.StrongTrans.

---

A strong natural transformation between oplax functors F and G is a natural transformation that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:

• a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B.
• a 2-isomorphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
• These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

Equations

• @CategoryTheory.Oplax.StrongOplaxNatTrans = @CategoryTheory.Oplax.StrongTrans

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : F.obj a ⟶ G.obj b} (h : CategoryStruct.comp (self.app a) (G.map g) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (CategoryStruct.comp (self.naturality g).hom h) = CategoryStruct.comp (self.naturality f).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c} (h : CategoryStruct.comp (self.app a) (CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z) : CategoryStruct.comp (self.naturality (CategoryStruct.comp f g)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.naturality g).hom) (CategoryStruct.comp (Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.naturality f).hom (G.map g)) (CategoryStruct.comp (Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a} (h : CategoryStruct.comp (self.app a) (CategoryStruct.id (G.obj a)) ⟶ Z) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapId a)) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (self.app a)).inv h))

structure CategoryTheory.Oplax.OplaxTrans.StrongCore {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) : Type (max (max u₁ v₁) w₂)

A structure on an oplax transformation that promotes it to a strong transformation.

See Pseudofunctor.StrongTrans.mkOfOplax.

• naturality {a b : B} (f : a ⟶ b) : CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryStruct.comp (η.app a) (G.map f)

  The underlying 2-isomorphisms of the naturality constraint.

• naturality_hom {a b : B} (f : a ⟶ b) : (self.naturality f).hom = η.naturality f

  The 2-isomorphisms agree with the underlying 2-morphism of the oplax transformation.

def CategoryTheory.Oplax.StrongTrans.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) : OplaxTrans F G

The underlying oplax natural transformation of a strong natural transformation.

Equations

• η.toOplax = { app := η.app, naturality := fun {a b : B} (f : a ⟶ b) => (η.naturality f).hom, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.toOplax_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : η.toOplax.naturality f = (η.naturality f).hom

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.toOplax_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) (a : B) : η.toOplax.app a = η.app a

def CategoryTheory.Oplax.StrongTrans.mkOfOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) (η' : OplaxTrans.StrongCore η) : StrongTrans F G

Construct a strong natural transformation from an oplax natural transformation whose naturality 2-morphism is an isomorphism.

Equations

• CategoryTheory.Oplax.StrongTrans.mkOfOplax η η' = { app := η.app, naturality := fun {a b : B} => η'.naturality, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

noncomputable def CategoryTheory.Oplax.StrongTrans.mkOfOplax' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxTrans F G) [∀ (a b : B) (f : a ⟶ b), IsIso (η.naturality f)] : StrongTrans F G

Construct a strong natural transformation from an oplax natural transformation whose naturality 2-morphism is an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Oplax.StrongTrans.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : StrongTrans F F

The identity strong natural transformation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.id_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((id F).naturality f).inv = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (Bicategory.rightUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (a : B) : (id F).app a = (OplaxTrans.id F).app a

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.id_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((id F).naturality f).hom = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (Bicategory.leftUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.id.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : (id F).toOplax = OplaxTrans.id F

instance CategoryTheory.Oplax.StrongTrans.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : Inhabited (StrongTrans F F)

Equations

• CategoryTheory.Oplax.StrongTrans.instInhabited F = { default := CategoryTheory.Oplax.StrongTrans.id F }

def CategoryTheory.Oplax.StrongTrans.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) : StrongTrans F H

Vertical composition of strong natural transformations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((η.vcomp θ).naturality f).hom = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom (θ.app b✝)) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).hom) (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).inv)))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.vcomp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) (a : B) : (η.vcomp θ).app a = (η.toOplax.vcomp θ.toOplax).app a

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((η.vcomp θ).naturality f).inv = CategoryStruct.comp (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).inv) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).inv (θ.app b✝)) (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).hom)))

def CategoryTheory.Oplax.StrongTrans.OplaxFunctor.instCategoryStruct {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (OplaxFunctor B C)

CategoryStruct on OplaxFunctor B C where the (1-)morphisms are given by strong transformations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.OplaxFunctor.comp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : StrongTrans X✝ Y✝) (θ : StrongTrans Y✝ Z✝) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.comp η θ).naturality f = (Bicategory.associator (X✝.map f) (η.app b✝) (θ.app b✝)).symm ≪≫ Bicategory.whiskerRightIso (η.naturality f) (θ.app b✝) ≪≫ Bicategory.associator (η.app a✝) (Y✝.map f) (θ.app b✝) ≪≫ Bicategory.whiskerLeftIso (η.app a✝) (θ.naturality f) ≪≫ (Bicategory.associator (η.app a✝) (θ.app a✝) (Z✝.map f)).symm

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.OplaxFunctor.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (a : B) : (CategoryStruct.id F).app a = (OplaxTrans.id F).app a

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.OplaxFunctor.comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : StrongTrans X✝ Y✝) (θ : StrongTrans Y✝ Z✝) (a : B) : (CategoryStruct.comp η θ).app a = (η.toOplax.vcomp θ.toOplax).app a

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.OplaxFunctor.id_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.id F).naturality f = Bicategory.rightUnitor (F.map f) ≪≫ (Bicategory.leftUnitor (F.map f)).symm

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (Bicategory.whiskerLeft f (θ.naturality h).hom) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ H.obj b} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality h).hom) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h✝)

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app {B : Type u_1} [Bicategory B] {G H : OplaxFunctor B Cat} (θ : StrongTrans G H) {a b : B} {a' : Cat} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) (X : ↑a') : CategoryStruct.comp ((θ.app b).map ((G.map₂ β).app (f.obj X))) ((θ.naturality h).hom.app (f.obj X)) = CategoryStruct.comp ((θ.naturality g).hom.app (f.obj X)) ((H.map₂ β).app ((θ.app a).obj (f.obj X)))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (Bicategory.whiskerRight (η.naturality g).hom h) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (Bicategory.associator (η.app a) (G.map g) h).inv))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality g).hom h) h✝) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map g) h).inv h✝)))

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app {B : Type u_1} [Bicategory B] {F G : OplaxFunctor B Cat} (η : StrongTrans F G) {a b : B} {a' : Cat} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') (X : ↑(F.obj a)) : CategoryStruct.comp (h.map ((η.app b).map ((F.map₂ β).app X))) (h.map ((η.naturality g).hom.app X)) = CategoryStruct.comp (h.map ((η.naturality f).hom.app X)) (CategoryStruct.comp ((Bicategory.associator (η.app a) (G.map f) h).hom.app X) (CategoryStruct.comp (h.map ((G.map₂ β).app ((η.app a).obj X))) ((Bicategory.associator (η.app a) (G.map g) h).inv.app X)))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.comp g h)).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom)) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (θ.naturality g).hom (H.map h))) (Bicategory.whiskerLeft f (Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ H.obj c} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.comp (H.map g) (H.map h))) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.comp g h)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom)) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (θ.naturality g).hom (H.map h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom) h✝)))))

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app {B : Type u_1} [Bicategory B] {G H : OplaxFunctor B Cat} (θ : StrongTrans G H) {a b c : B} {a' : Cat} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) (X : ↑a') : CategoryStruct.comp ((θ.naturality (CategoryStruct.comp g h)).hom.app (f.obj X)) ((H.mapComp g h).app ((θ.app a).obj (f.obj X))) = CategoryStruct.comp ((θ.app c).map ((G.mapComp g h).app (f.obj X))) (CategoryStruct.comp ((Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom.app (f.obj X)) (CategoryStruct.comp ((θ.naturality h).hom.app ((G.map g).obj (f.obj X))) (CategoryStruct.comp ((Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv.app (f.obj X)) (CategoryStruct.comp ((H.map h).map ((θ.naturality g).hom.app (f.obj X))) ((Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom.app (f.obj X))))))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.comp f g)).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.comp f g)) h).hom (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapComp f g) h))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (η.naturality g).hom h)) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (Bicategory.associator (η.app a) (CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.comp (G.map f) (G.map g)) h) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.comp f g)).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.comp f g)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapComp f g) h)) h✝)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (η.naturality g).hom h)) (CategoryStruct.comp (Bicategory.associator (F.map f) (CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (CategoryStruct.comp (G.map f) (G.map g)) h).hom h✝))))))))

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app {B : Type u_1} [Bicategory B] {F G : OplaxFunctor B Cat} (η : StrongTrans F G) {a b c : B} {a' : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') (X : ↑(F.obj a)) : CategoryStruct.comp (h.map ((η.naturality (CategoryStruct.comp f g)).hom.app X)) (CategoryStruct.comp ((Bicategory.associator (η.app a) (G.map (CategoryStruct.comp f g)) h).hom.app X) (h.map ((G.mapComp f g).app ((η.app a).obj X)))) = CategoryStruct.comp (h.map ((η.app c).map ((F.mapComp f g).app X))) (CategoryStruct.comp (h.map ((Bicategory.associator (F.map f) (F.map g) (η.app c)).hom.app X)) (CategoryStruct.comp ((Bicategory.associator (F.map f) (CategoryStruct.comp (F.map g) (η.app c)) h).hom.app X) (CategoryStruct.comp (h.map ((η.naturality g).hom.app ((F.map f).obj X))) (CategoryStruct.comp ((Bicategory.associator (F.map f) (CategoryStruct.comp (η.app b) (G.map g)) h).inv.app X) (CategoryStruct.comp (h.map ((Bicategory.associator (F.map f) (η.app b) (G.map g)).inv.app X)) (CategoryStruct.comp (h.map ((G.map g).map ((η.naturality f).hom.app X))) (CategoryStruct.comp (h.map ((Bicategory.associator (η.app a) (G.map f) (G.map g)).hom.app X)) ((Bicategory.associator (η.app a) (CategoryStruct.comp (G.map f) (G.map g)) h).hom.app X))))))))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a)).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) {Z : a' ⟶ H.obj a} (h : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.id (H.obj a))) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv) h))

theorem CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app {B : Type u_1} [Bicategory B] {G H : OplaxFunctor B Cat} (θ : StrongTrans G H) {a : B} {a' : Cat} (f : a' ⟶ G.obj a) (X : ↑a') : CategoryStruct.comp ((θ.naturality (CategoryStruct.id a)).hom.app (f.obj X)) ((H.mapId a).app ((θ.app a).obj (f.obj X))) = CategoryStruct.comp ((θ.app a).map ((G.mapId a).app (f.obj X))) (CategoryStruct.comp ((Bicategory.leftUnitor (θ.app a)).hom.app (f.obj X)) ((Bicategory.rightUnitor (θ.app a)).inv.app (f.obj X)))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)).hom f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom))

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') {Z : F.obj a ⟶ a'} (h : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.id (G.obj a)) f) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)).hom f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f)) h)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (CategoryStruct.comp (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom h)))

theorem CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app {B : Type u_1} [Bicategory B] {F G : OplaxFunctor B Cat} (η : StrongTrans F G) {a : B} {a' : Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)) : CategoryStruct.comp (f.map ((η.naturality (CategoryStruct.id a)).hom.app X)) (CategoryStruct.comp ((Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom.app X) (f.map ((G.mapId a).app ((η.app a).obj X)))) = CategoryStruct.comp (f.map ((η.app a).map ((F.mapId a).app X))) (CategoryStruct.comp (f.map ((Bicategory.leftUnitor (η.app a)).hom.app X)) (CategoryStruct.comp (f.map ((Bicategory.rightUnitor (η.app a)).inv.app X)) ((Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom.app X)))