Oplax transformations between oplax functors

Just as there are natural transformations between functors, there are oplax transformations between oplax functors. The equality in the naturality of natural transformations is replaced by a specified 2-morphism F.map f ≫ app b ⟶ app a ≫ G.map f in the case of oplax natural transformations.

Main definitions

• OplaxTrans F G : oplax transformations between oplax functors F and G

Using this, we define a category instance on OplaxTrans F G, with composition given by vertical composition of oplax transformations.

TODO

This file could also include lax and strong transformations between oplax functors.

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

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

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

  The component 1-morphisms of an oplax transformation.

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

  The 2-morphisms underlying the oplax naturality constraint.

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

  Naturality of the oplax naturality constraint.

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

  Oplax unity.

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

  Oplax functoriality.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Alias of CategoryTheory.Oplax.OplaxTrans.

---

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity oplax transformation.

Equations

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

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

Equations

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

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

Vertical composition of oplax transformations.

Equations

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

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

Equations

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

@[simp]

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