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.LaxTrans F G: lax transformations between oplax functors F and G. The naturality condition is given by a 2-morphism app a ≫ G.map f ⟶ F.map f ≫ app b for each 1-morphism f : a ⟶ b.
• 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. The naturality condition is given by a 2-isomorphism F.map f ≫ app b ≅ app a ≫ G.map f for each 1-morphism f : a ⟶ b.

Using these, we define three (scoped) CategoryStruct instances on B ⥤ᵒᵖᴸ C, in the Oplax.LaxTrans, Oplax.OplaxTrans, and Oplax.StrongTrans namespaces. The arrows in these CategoryStruct instances are given by lax transformations, oplax transformations, and strong transformations respectively.

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

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

References

• Niles Johnson, Donald Yau, 2-Dimensional Categories

structure CategoryTheory.Oplax.LaxTrans {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 a lax 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 : app a ≫ G.map f ⟶ F.map f ≫ app b for each 1-morphism f : a ⟶ b. These 2-morphisms 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 lax transformation.

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

  The 2-morphisms underlying the lax naturality constraint.

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity lax transformation.

@[implicit_reducible]

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

@[reducible, inline]

abbrev CategoryTheory.Oplax.LaxTrans.vCompApp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) (a : B) : F.obj a ⟶ H.obj a

Auxiliary definition for vComp.

@[reducible, inline]

abbrev CategoryTheory.Oplax.LaxTrans.vCompNaturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b : B} (f : a ⟶ b) : CategoryStruct.comp (CategoryStruct.comp (η.app a) (θ.app a)) (H.map f) ⟶ CategoryStruct.comp (F.map f) (CategoryStruct.comp (η.app b) (θ.app b))

Auxiliary definition for vComp.

theorem CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b : B} {f g : a ⟶ b} (β : f ⟶ g) : CategoryStruct.comp (η.vCompNaturality θ f) (Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b)) = CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β)) (η.vCompNaturality θ g)

theorem CategoryTheory.Oplax.LaxTrans.vComp_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) (a : B) : CategoryStruct.comp (η.vCompNaturality θ (CategoryStruct.id a)) (Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a)) = CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a)) (CategoryStruct.comp (Bicategory.rightUnitor (η.vCompApp θ a)).hom (Bicategory.leftUnitor (η.vCompApp θ a)).inv)

theorem CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (η.vCompNaturality θ (CategoryStruct.comp f g)) (Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c)) = CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g)) (CategoryStruct.comp (Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g)) (Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).inv))))

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

Vertical composition of lax transformations.

@[implicit_reducible]

def CategoryTheory.Oplax.LaxTrans.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 lax transformations.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Oplax.LaxTrans.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.leftUnitor (F.map f)).hom (Bicategory.rightUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.Oplax.LaxTrans.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)

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 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 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_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)
• 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))))

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

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

@[implicit_reducible]

instance CategoryTheory.Oplax.OplaxTrans.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F : OplaxFunctor B C} : Inhabited (OplaxTrans F 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.

@[implicit_reducible]

def CategoryTheory.Oplax.OplaxTrans.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₁} (OplaxFunctor B C)

CategoryStruct on B ⥤ᵒᵖᴸ C where the (1-)morphisms are given by oplax transformations.

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.categoryStruct_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)))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.categoryStruct_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.categoryStruct_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.categoryStruct_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

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

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

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

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 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.

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

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

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

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

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.

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.

@[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_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.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : (id F).toOplax = OplaxTrans.id F

@[implicit_reducible]

instance CategoryTheory.Oplax.StrongTrans.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) : Inhabited (StrongTrans F 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.

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

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

@[implicit_reducible]

def CategoryTheory.Oplax.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₁} (OplaxFunctor B C)

CategoryStruct on B ⥤ᵒᵖᴸ C where the (1-)morphisms are given by strong transformations.

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.categoryStruct_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.categoryStruct_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.categoryStruct_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.categoryStruct_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.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).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.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.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.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.toNatTrans.app (f.toFunctor.obj X)) ((H.mapComp g h).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) = CategoryStruct.comp ((θ.app c).toFunctor.map ((G.mapComp g h).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.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.toFunctor.map ((η.naturality (CategoryStruct.comp f g)).hom.toNatTrans.app X)) (h.toFunctor.map ((G.mapComp f g).toNatTrans.app ((η.app a).toFunctor.obj X))) = CategoryStruct.comp (h.toFunctor.map ((η.app c).toFunctor.map ((F.mapComp f g).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.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.toNatTrans.app (f.toFunctor.obj X)) ((H.mapId a).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) = CategoryStruct.comp ((θ.app a).toFunctor.map ((G.mapId a).toNatTrans.app (f.toFunctor.obj X))) (CategoryStruct.comp (eqToHom ⋯) (eqToHom ⋯))

@[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.toFunctor.map ((η.naturality (CategoryStruct.id a)).hom.toNatTrans.app X)) (f.toFunctor.map ((G.mapId a).toNatTrans.app ((η.app a).toFunctor.obj X))) = CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).toNatTrans.app X))) (CategoryStruct.comp (f.toFunctor.map (eqToHom ⋯)) (f.toFunctor.map (eqToHom ⋯)))