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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.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) → CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ⟶ CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
• naturality_naturality : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g) = CategoryTheory.CategoryStruct.comp (self.naturality f) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
• naturality_id : ∀ (a : B), CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
• naturality_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

@[simp]

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

@[simp]

theorem CategoryTheory.OplaxNatTrans.naturality_id {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.OplaxNatTrans F G) (a : B) : CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.OplaxNatTrans.id {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : ∀ {x x_1 : B} (f : x ⟶ x_1), (CategoryTheory.OplaxNatTrans.id F).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.OplaxNatTrans.vcomp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans F G) (θ : CategoryTheory.OplaxNatTrans G H) : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans F G) (θ : CategoryTheory.OplaxNatTrans G H) (a : B) : (η.vcomp θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)

@[simp]

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

instance CategoryTheory.OplaxNatTrans.instCategoryStructOplaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (CategoryTheory.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₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : CategoryTheory.CategoryStruct.id F = CategoryTheory.OplaxNatTrans.id F

@[simp]

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

structure CategoryTheory.OplaxNatTrans.StrongCore {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.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) → CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f)
• naturality_hom : ∀ {a b : B} (f : a ⟶ b), (self.naturality f).hom = η.naturality f

@[simp]

theorem CategoryTheory.OplaxNatTrans.StrongCore.naturality_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : CategoryTheory.OplaxNatTrans F G} (self : η.StrongCore) {a : B} {b : B} (f : a ⟶ b) : (self.naturality f).hom = η.naturality f