Strong transformations of pseudofunctors

There are three types of transformations between pseudofunctors, depending on the direction or invertibility of the 2-morphism witnessing the naturality condition.

In this file we define strong transformations, which require the 2-morphism to be invertible.

Main definitions

• Pseudofunctor.StrongTrans F G: strong transformations between pseudofunctors F and G.
• Pseudofunctor.mkOfOplax η η': Given two pseudofunctors, and a strong transformation η between their underlying oplax functors, mkOfOplax lifts this to a strong transformation between the pseudofunctors.
• Pseudofunctor.StrongTrans.vcomp η θ: the vertical composition of strong transformations η and θ.

Using this we obtain a (scoped) CategoryStruct on pseudofunctors, where the arrows are given by strong transformations. To access this instance, run open scoped Pseudofunctor.StrongTrans. See Pseudofunctor.StrongTrans.categoryStruct.

References

• Niles Johnson, Donald Yau, 2-Dimensional Categories

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

A strong transformation between pseudofunctors 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

  The component 1-morphisms of a strong 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-isomorphisms underlying the strong 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).hom = CategoryStruct.comp (self.naturality f).hom (Bicategory.whiskerLeft (self.app a) (G.map₂ η))

  Naturality of the strong naturality constraint.

• naturality_id (a : B) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)).hom (Bicategory.whiskerLeft (self.app a) (G.mapId a).hom) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (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)).hom (Bicategory.whiskerLeft (self.app a) (G.mapComp f g).hom) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (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))))

  Oplax functoriality.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (self : F.StrongTrans 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).hom) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (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)))))

Oplax functoriality.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (self : F.StrongTrans 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)

Naturality of the strong naturality constraint.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (self : F.StrongTrans 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).hom) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (self.app a)).inv h))

Oplax unity.

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

The strong transformation of oplax functors induced by a strong transformation of pseudofunctors.

Equations

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

@[simp]

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

@[simp]

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

instance CategoryTheory.Pseudofunctor.StrongTrans.hasCoeToOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} : Coe (F.StrongTrans G) (Oplax.StrongTrans F.toOplax G.toOplax)

Equations

• CategoryTheory.Pseudofunctor.StrongTrans.hasCoeToOplax = { coe := CategoryTheory.Pseudofunctor.StrongTrans.toOplax }

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

Construct a strong transformation of pseudofunctors from a strong transformation of the underlying oplax functors.

Equations

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

@[simp]

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

@[simp]

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

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

The identity strong transformation.

Equations

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

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

Equations

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

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

Vertical composition of strong transformations.

Equations

• η.vcomp θ = CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax (η.toOplax.vcomp θ.toOplax)

def CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct {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₁} (Pseudofunctor B C)

CategoryStruct on 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.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : Pseudofunctor B C} (η : X✝.StrongTrans Y✝) (θ : Y✝.StrongTrans Z✝) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((CategoryStruct.comp η θ).naturality f).hom = CategoryStruct.comp (Bicategory.associator (X✝.map f) (η.app b✝) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom (θ.app b✝)) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (Y✝.map f) (θ.app b✝)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).hom) (Bicategory.associator (η.app a✝) (θ.app a✝) (Z✝.map f)).inv)))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) (a : B) : (CategoryStruct.id F).app a = CategoryStruct.id (F.obj a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : Pseudofunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (a : B) : (CategoryStruct.comp η θ).app a = CategoryStruct.comp (η.app a) (θ.app a)

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app {B : Type u_1} [Bicategory B] {G H : Pseudofunctor B Cat} (θ : G ⟶ H) {a b : B} {a' : Cat} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) (X : ↑a') : CategoryStruct.comp ((θ.app b).toFunctor.map ((G.map₂ β).toNatTrans.app (f.toFunctor.obj X))) ((θ.naturality h).hom.toNatTrans.app (f.toFunctor.obj X)) = CategoryStruct.comp ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X)) ((H.map₂ β).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X)))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (η : 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.toFunctor.map ((η.app b).toFunctor.map ((F.map₂ β).toNatTrans.app X))) (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app X)) = CategoryStruct.comp (h.toFunctor.map ((η.naturality f).hom.toNatTrans.app X)) (h.toFunctor.map ((G.map₂ β).toNatTrans.app ((η.app a).toFunctor.obj X)))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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).hom)) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h).hom (θ.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.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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).hom)) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h).hom (θ.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.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app {B : Type u_1} [Bicategory B] {G H : Pseudofunctor B Cat} (θ : 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.toNatTrans.app (f.toFunctor.obj X)) ((H.mapComp g h).hom.toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) = CategoryStruct.comp ((θ.app c).toFunctor.map ((G.mapComp g h).hom.toNatTrans.app (f.toFunctor.obj X))) (CategoryStruct.comp ((θ.naturality h).hom.toNatTrans.app ((G.map g).toFunctor.obj (f.toFunctor.obj X))) ((H.map h).toFunctor.map ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X))))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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).hom h))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g).hom (η.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.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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).hom h)) h✝)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapComp f g).hom (η.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.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (η : 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.toFunctor.map ((η.naturality (CategoryStruct.comp f g)).hom.toNatTrans.app X)) (h.toFunctor.map ((G.mapComp f g).hom.toNatTrans.app ((η.app a).toFunctor.obj X))) = CategoryStruct.comp (h.toFunctor.map ((η.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X))) (CategoryStruct.comp (h.toFunctor.map (CategoryStruct.id ((η.app c).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X))))) (CategoryStruct.comp (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X))) (CategoryStruct.comp (h.toFunctor.map (CategoryStruct.id ((G.map g).toFunctor.obj ((η.app b).toFunctor.obj ((F.map f).toFunctor.obj X))))) (CategoryStruct.comp (h.toFunctor.map ((G.map g).toFunctor.map ((η.naturality f).hom.toNatTrans.app X))) (h.toFunctor.map (CategoryStruct.id ((G.map g).toFunctor.obj ((G.map f).toFunctor.obj ((η.app a).toFunctor.obj X)))))))))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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).hom)) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a).hom (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : Pseudofunctor B C} (θ : 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).hom)) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a).hom (θ.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.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app {B : Type u_1} [Bicategory B] {G H : Pseudofunctor B Cat} (θ : G ⟶ H) {a : B} {a' : Cat} (f : a' ⟶ G.obj a) (X : ↑a') : CategoryStruct.comp ((θ.naturality (CategoryStruct.id a)).hom.toNatTrans.app (f.toFunctor.obj X)) ((H.mapId a).hom.toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) = (θ.app a).toFunctor.map ((G.mapId a).hom.toNatTrans.app (f.toFunctor.obj X))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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).hom f))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a).hom (η.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.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : 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).hom f)) h)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a).hom (η.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.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (η : F ⟶ G) {a : B} {a' : Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)) : CategoryStruct.comp (f.toFunctor.map ((η.naturality (CategoryStruct.id a)).hom.toNatTrans.app X)) (f.toFunctor.map ((G.mapId a).hom.toNatTrans.app ((η.app a).toFunctor.obj X))) = CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X))) (CategoryStruct.comp (f.toFunctor.map (CategoryStruct.id ((η.app a).toFunctor.obj ((CategoryStruct.id (F.obj a)).toFunctor.obj X)))) (f.toFunctor.map (CategoryStruct.id ((η.app a).toFunctor.obj X))))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) (a : B) : (α.naturality (CategoryStruct.id a)).hom = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (α.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (α.app a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (α.app a)).inv (Bicategory.whiskerLeft (α.app a) (G.mapId a).inv)))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) : (α.naturality (CategoryStruct.id a)).hom.toNatTrans.app X = CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) ((G.mapId a).inv.toNatTrans.app ((α.app a).toFunctor.obj X))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) {Z : ↑(G.obj a)} (h : (G.map (CategoryStruct.id a)).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp ((α.naturality (CategoryStruct.id a)).hom.toNatTrans.app X) h = CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) (CategoryStruct.comp ((G.mapId a).inv.toNatTrans.app ((α.app a).toFunctor.obj X)) h)

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

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) (a : B) : α.naturality (CategoryStruct.id a) = Bicategory.whiskerRightIso (F.mapId a) (α.app a) ≪≫ Bicategory.leftUnitor (α.app a) ≪≫ (Bicategory.rightUnitor (α.app a)).symm ≪≫ Bicategory.whiskerLeftIso (α.app a) (G.mapId a).symm

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) (a : B) : (α.naturality (CategoryStruct.id a)).inv = CategoryStruct.comp (Bicategory.whiskerLeft (α.app a) (G.mapId a).hom) (CategoryStruct.comp (Bicategory.rightUnitor (α.app a)).hom (CategoryStruct.comp (Bicategory.leftUnitor (α.app a)).inv (Bicategory.whiskerRight (F.mapId a).inv (α.app a))))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) : (α.naturality (CategoryStruct.id a)).inv.toNatTrans.app X = CategoryStruct.comp ((G.mapId a).hom.toNatTrans.app ((α.app a).toFunctor.obj X)) ((α.app a).toFunctor.map ((F.mapId a).inv.toNatTrans.app X))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) {Z : ↑(G.obj a)} (h : (α.app a).toFunctor.obj ((F.map (CategoryStruct.id a)).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp ((α.naturality (CategoryStruct.id a)).inv.toNatTrans.app X) h = CategoryStruct.comp ((G.mapId a).hom.toNatTrans.app ((α.app a).toFunctor.obj X)) (CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h)

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

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) : (α.naturality g).hom = CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η.inv) (α.app b)) (CategoryStruct.comp (α.naturality f).hom (Bicategory.whiskerLeft (α.app a) (G.map₂ η.hom)))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) (X : ↑(F.obj a)) : (α.naturality g).hom.toNatTrans.app X = CategoryStruct.comp ((α.app b).toFunctor.map ((F.map₂ η.inv).toNatTrans.app X)) (CategoryStruct.comp ((α.naturality f).hom.toNatTrans.app X) ((G.map₂ η.hom).toNatTrans.app ((α.app a).toFunctor.obj X)))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) (X : ↑(F.obj a)) {Z : ↑(G.obj b)} (h : (G.map g).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app X) h = CategoryStruct.comp ((α.app b).toFunctor.map ((F.map₂ η.inv).toNatTrans.app X)) (CategoryStruct.comp ((α.naturality f).hom.toNatTrans.app X) (CategoryStruct.comp ((G.map₂ η.hom).toNatTrans.app ((α.app a).toFunctor.obj X)) h))

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

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) : α.naturality g = Bicategory.whiskerRightIso (F.map₂Iso η.symm) (α.app b) ≪≫ α.naturality f ≪≫ Bicategory.whiskerLeftIso (α.app a) (G.map₂Iso η)

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) : (α.naturality g).inv = CategoryStruct.comp (Bicategory.whiskerLeft (α.app a) (G.map₂ η.inv)) (CategoryStruct.comp (α.naturality f).inv (Bicategory.whiskerRight (F.map₂ η.hom) (α.app b)))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : (α.naturality (CategoryStruct.comp f g)).hom = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (α.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (α.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (α.naturality g).hom) (CategoryStruct.comp (Bicategory.associator (F.map f) (α.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (α.naturality f).hom (G.map g)) (CategoryStruct.comp (Bicategory.associator (α.app a) (G.map f) (G.map g)).hom (Bicategory.whiskerLeft (α.app a) (G.mapComp f g).inv))))))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) : (α.naturality (CategoryStruct.comp f g)).hom.toNatTrans.app X = CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) (CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).hom.toNatTrans.app X)) ((G.mapComp f g).inv.toNatTrans.app ((α.app a).toFunctor.obj X))))

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

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) {Z : ↑(G.obj c)} (h : (G.map (CategoryStruct.comp f g)).toFunctor.obj ((α.app a).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp ((α.naturality (CategoryStruct.comp f g)).hom.toNatTrans.app X) h = CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) (CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).hom.toNatTrans.app X)) (CategoryStruct.comp ((G.mapComp f g).inv.toNatTrans.app ((α.app a).toFunctor.obj X)) h)))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : α.naturality (CategoryStruct.comp f g) = Bicategory.whiskerRightIso (F.mapComp f g) (α.app c) ≪≫ Bicategory.associator (F.map f) (F.map g) (α.app c) ≪≫ Bicategory.whiskerLeftIso (F.map f) (α.naturality g) ≪≫ (Bicategory.associator (F.map f) (α.app b) (G.map g)).symm ≪≫ Bicategory.whiskerRightIso (α.naturality f) (G.map g) ≪≫ Bicategory.associator (α.app a) (G.map f) (G.map g) ≪≫ Bicategory.whiskerLeftIso (α.app a) (G.mapComp f g).symm

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : (α.naturality (CategoryStruct.comp f g)).inv = CategoryStruct.comp (Bicategory.whiskerLeft (α.app a) (G.mapComp f g).hom) (CategoryStruct.comp (Bicategory.associator (α.app a) (G.map f) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (α.naturality f).inv (G.map g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (α.app b) (G.map g)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (α.naturality g).inv) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (α.app c)).inv (Bicategory.whiskerRight (F.mapComp f g).inv (α.app c)))))))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) : (α.naturality (CategoryStruct.comp f g)).inv.toNatTrans.app X = CategoryStruct.comp ((G.mapComp f g).hom.toNatTrans.app ((α.app a).toFunctor.obj X)) (CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).inv.toNatTrans.app X)) (CategoryStruct.comp ((α.naturality g).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) ((α.app c).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))))

theorem CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc {B : Type u_1} [Bicategory B] {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)) {Z : ↑(G.obj c)} (h : (α.app c).toFunctor.obj ((F.map (CategoryStruct.comp f g)).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp ((α.naturality (CategoryStruct.comp f g)).inv.toNatTrans.app X) h = CategoryStruct.comp ((G.mapComp f g).hom.toNatTrans.app ((α.app a).toFunctor.obj X)) (CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).inv.toNatTrans.app X)) (CategoryStruct.comp ((α.naturality g).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) h)))

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