Oplax natural transformations

Just as there are natural transformations between functors, there are oplax natural 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

• OplaxNatTrans F G : oplax natural transformations between oplax functors F and G
• OplaxNatTrans.vcomp η θ : the vertical composition of oplax natural transformations η and θ
• OplaxNatTrans.category F G : the category structure on the oplax natural transformations between F and G

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

If η is an oplax natural 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
• 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) = 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.OplaxNatTrans.naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxNatTrans 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.OplaxNatTrans.naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxNatTrans 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.OplaxNatTrans.naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : OplaxNatTrans 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))

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

The identity oplax natural transformation.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.OplaxNatTrans.instInhabited F = { default := CategoryTheory.OplaxNatTrans.id F }

@[simp]

theorem CategoryTheory.OplaxNatTrans.whiskerLeft_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerLeft_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.whiskerLeft_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.whiskerLeft_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerLeft_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.whiskerRight_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans 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.OplaxNatTrans.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : OplaxNatTrans F G) (θ : OplaxNatTrans G H) : OplaxNatTrans F H

Vertical composition of oplax natural transformations.

Equations

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

@[simp]

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

@[simp]

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

instance CategoryTheory.OplaxNatTrans.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.OplaxNatTrans.instCategoryStructOplaxFunctor_id (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F : OplaxFunctor B C) : CategoryStruct.id F = id F

@[simp]

theorem CategoryTheory.OplaxNatTrans.instCategoryStructOplaxFunctor_comp (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxNatTrans X✝ Y✝) (θ : OplaxNatTrans Y✝ Z✝) : CategoryStruct.comp η θ = η.vcomp θ

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

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

See StrongNatTrans.mkOfOplax.

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