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 CategoryStruct on pseudofunctors, where the arrows are given by strong transformations. See Pseudofunctor.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)))))

@[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)

@[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))

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 underlying oplax transformation of a strong transformation.

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 Pseudofunctor 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_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.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_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_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.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).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.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.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.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.app (f.obj X)) ((H.mapComp g h).hom.app ((θ.app a).obj (f.obj X))) = CategoryStruct.comp ((θ.app c).map ((G.mapComp g h).hom.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.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.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).hom.app ((η.app a).obj X)))) = CategoryStruct.comp (h.map ((η.app c).map ((F.mapComp f g).hom.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.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.app (f.obj X)) ((H.mapId a).hom.app ((θ.app a).obj (f.obj X))) = CategoryStruct.comp ((θ.app a).map ((G.mapId a).hom.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.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.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).hom.app ((η.app a).obj X)))) = CategoryStruct.comp (f.map ((η.app a).map ((F.mapId a).hom.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)))