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

• app : (a : B) → (↑F.toPrelaxFunctor).obj a ⟶ (↑G.toPrelaxFunctor).obj a
• naturality : {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp ((↑F.toPrelaxFunctor).map f) (s.app b) ⟶ CategoryTheory.CategoryStruct.comp (s.app a) ((↑G.toPrelaxFunctor).map f)
• naturality_naturality : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor η) (s.app b)) (CategoryTheory.OplaxNatTrans.naturality s g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality s f) (CategoryTheory.Bicategory.whiskerLeft (s.app a) (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor η))
• naturality_id : ∀ (a : B), CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality s (CategoryTheory.CategoryStruct.id a)) (CategoryTheory.Bicategory.whiskerLeft (s.app a) (CategoryTheory.OplaxFunctor.mapId G a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId F a) (s.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (s.app a)).hom (CategoryTheory.Bicategory.rightUnitor (s.app a)).inv)
• naturality_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality s (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Bicategory.whiskerLeft (s.app a) (CategoryTheory.OplaxFunctor.mapComp G f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp F f g) (s.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (s.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (CategoryTheory.OplaxNatTrans.naturality s g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (s.app b) ((↑G.toPrelaxFunctor).map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality s f) ((↑G.toPrelaxFunctor).map g)) (CategoryTheory.Bicategory.associator (s.app a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom))))

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.

@[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.toPrelaxFunctor).obj a ⟶ (↑G.toPrelaxFunctor).obj a} (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.id ((↑G.toPrelaxFunctor).obj a)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality self (CategoryTheory.CategoryStruct.id a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (CategoryTheory.OplaxFunctor.mapId G a)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId F 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))

@[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.toPrelaxFunctor).obj a ⟶ (↑G.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.comp ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality self (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (CategoryTheory.OplaxFunctor.mapComp G f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp F f g) (self.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (self.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (CategoryTheory.OplaxNatTrans.naturality self g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (self.app b) ((↑G.toPrelaxFunctor).map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality self f) ((↑G.toPrelaxFunctor).map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom h)))))

@[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.toPrelaxFunctor).obj a ⟶ (↑G.toPrelaxFunctor).obj b} (h : CategoryTheory.CategoryStruct.comp (self.app a) ((↑G.toPrelaxFunctor).map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor η) (self.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality self g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality self f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor η)) h)

@[simp]

theorem CategoryTheory.OplaxNatTrans.id_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) : CategoryTheory.OplaxNatTrans.naturality (CategoryTheory.OplaxNatTrans.id F) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑F.toPrelaxFunctor).map f)).hom (CategoryTheory.Bicategory.leftUnitor ((↑F.toPrelaxFunctor).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.toPrelaxFunctor).obj a)

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.

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

@[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.toPrelaxFunctor).obj a) {g : a ⟶ b} {h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ (↑H.toPrelaxFunctor).obj b} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) ((↑H.toPrelaxFunctor).map h)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor β) (θ.app b))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ h)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.PrelaxFunctor.map₂ H.toPrelaxFunctor β))) h)

@[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.toPrelaxFunctor).obj a) {g : a ⟶ b} {h : a ⟶ b} (β : g ⟶ h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor β) (θ.app b))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ g)) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.PrelaxFunctor.map₂ H.toPrelaxFunctor β)))

@[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.toPrelaxFunctor).obj b ⟶ a') {Z : (↑F.toPrelaxFunctor).obj a ⟶ a'} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) ((↑G.toPrelaxFunctor).map g)) h ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor β) (η.app b)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η g) h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map f) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor β) h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map g) h).inv 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.toPrelaxFunctor).obj b ⟶ a') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor β) (η.app b)) h) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map f) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ G.toPrelaxFunctor β) h)) (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map g) h).inv))

@[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.toPrelaxFunctor).obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ (↑H.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.comp ((↑H.toPrelaxFunctor).map g) ((↑H.toPrelaxFunctor).map h))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ (CategoryTheory.CategoryStruct.comp g h))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.OplaxFunctor.mapComp H g h))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp G g h) (θ.app c))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator ((↑G.toPrelaxFunctor).map g) ((↑G.toPrelaxFunctor).map h) (θ.app c)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft ((↑G.toPrelaxFunctor).map g) (CategoryTheory.OplaxNatTrans.naturality θ h))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator ((↑G.toPrelaxFunctor).map g) (θ.app b) ((↑H.toPrelaxFunctor).map h)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality θ g) ((↑H.toPrelaxFunctor).map h))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (θ.app a) ((↑H.toPrelaxFunctor).map g) ((↑H.toPrelaxFunctor).map h)).hom) 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.toPrelaxFunctor).obj a) (g : a ⟶ b) (h : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ (CategoryTheory.CategoryStruct.comp g h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.OplaxFunctor.mapComp H g h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp G g h) (θ.app c))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator ((↑G.toPrelaxFunctor).map g) ((↑G.toPrelaxFunctor).map h) (θ.app c)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft ((↑G.toPrelaxFunctor).map g) (CategoryTheory.OplaxNatTrans.naturality θ h))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator ((↑G.toPrelaxFunctor).map g) (θ.app b) ((↑H.toPrelaxFunctor).map h)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality θ g) ((↑H.toPrelaxFunctor).map h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (θ.app a) ((↑H.toPrelaxFunctor).map g) ((↑H.toPrelaxFunctor).map 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.toPrelaxFunctor).obj c ⟶ a') {Z : (↑F.toPrelaxFunctor).obj a ⟶ a'} (h : CategoryTheory.CategoryStruct.comp (η.app a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)) h) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η (CategoryTheory.CategoryStruct.comp f g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g)) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp G f g) h)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp F f g) (η.app c)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp ((↑F.toPrelaxFunctor).map g) (η.app c)) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η g) h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp (η.app b) ((↑G.toPrelaxFunctor).map g)) h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g)).inv h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) ((↑G.toPrelaxFunctor).map g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.comp ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)) 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.toPrelaxFunctor).obj c ⟶ a') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η (CategoryTheory.CategoryStruct.comp f g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g)) h).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp G f g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp F f g) (η.app c)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp ((↑F.toPrelaxFunctor).map g) (η.app c)) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η g) h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp (η.app b) ((↑G.toPrelaxFunctor).map g)) h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g)).inv h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) ((↑G.toPrelaxFunctor).map g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom h) (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.comp ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)) h).hom)))))))

@[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.toPrelaxFunctor).obj a) {Z : a' ⟶ (↑H.toPrelaxFunctor).obj a} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.id ((↑H.toPrelaxFunctor).obj a))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ (CategoryTheory.CategoryStruct.id a))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.OplaxFunctor.mapId H a))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId G 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.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.toPrelaxFunctor).obj a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ (CategoryTheory.CategoryStruct.id a))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (CategoryTheory.OplaxFunctor.mapId H a))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId G 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.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.toPrelaxFunctor).obj a ⟶ a') {Z : (↑F.toPrelaxFunctor).obj a ⟶ a'} (h : CategoryTheory.CategoryStruct.comp (η.app a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((↑G.toPrelaxFunctor).obj a)) f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η (CategoryTheory.CategoryStruct.id a)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a)) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId G a) f)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId F 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.toPrelaxFunctor).obj a)) f).hom 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.toPrelaxFunctor).obj a ⟶ a') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η (CategoryTheory.CategoryStruct.id a)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a)) f).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId G a) f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId F 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.toPrelaxFunctor).obj a)) f).hom))

@[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) : CategoryTheory.OplaxNatTrans.naturality (CategoryTheory.OplaxNatTrans.vcomp η θ) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) (θ.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.OplaxNatTrans.naturality θ f)) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f)).inv)))

@[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) : (CategoryTheory.OplaxNatTrans.vcomp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)

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.

@[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 η θ = CategoryTheory.OplaxNatTrans.vcomp η θ

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)

theorem CategoryTheory.OplaxNatTrans.Modification.ext_iff {B : Type u₁} : ∀ {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C} {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (x y : CategoryTheory.OplaxNatTrans.Modification η θ), x = y ↔ x.app = y.app

theorem CategoryTheory.OplaxNatTrans.Modification.ext {B : Type u₁} : ∀ {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C} {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (x y : CategoryTheory.OplaxNatTrans.Modification η θ), x.app = y.app → x = y

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

• app : (a : B) → η.app a ⟶ θ.app a
• naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (s.app b)) (CategoryTheory.OplaxNatTrans.naturality θ f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality η f) (CategoryTheory.Bicategory.whiskerRight (s.app a) ((↑G.toPrelaxFunctor).map f))

A modification Γ between oplax natural transformations η and θ consists of a family of 2-morphisms Γ.app a : η.app a ⟶ θ.app a, which satisfies the equation (F.map f ◁ app b) ≫ θ.naturality f = η.naturality f ≫ (app a ▷ G.map f) for each 1-morphism f : a ⟶ b.

@[simp]

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

@[simp]

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

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

The identity modification.

instance CategoryTheory.OplaxNatTrans.Modification.instInhabitedModification {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) : Inhabited (CategoryTheory.OplaxNatTrans.Modification η η)

@[simp]

theorem CategoryTheory.OplaxNatTrans.Modification.whiskerLeft_naturality_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification η θ) {b : B} {c : B} {a' : C} (f : a' ⟶ (↑F.toPrelaxFunctor).obj b) (g : b ⟶ c) {Z : a' ⟶ (↑G.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app b) ((↑G.toPrelaxFunctor).map g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map g) (Γ.app c))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality η g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) ((↑G.toPrelaxFunctor).map g))) h)

@[simp]

theorem CategoryTheory.OplaxNatTrans.Modification.whiskerLeft_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification η θ) {b : B} {c : B} {a' : C} (f : a' ⟶ (↑F.toPrelaxFunctor).obj b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map g) (Γ.app c))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality θ g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.OplaxNatTrans.naturality η g)) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) ((↑G.toPrelaxFunctor).map g)))

@[simp]

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

@[simp]

theorem CategoryTheory.OplaxNatTrans.Modification.whiskerRight_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification η θ) {a : B} {b : B} {a' : C} (f : a ⟶ b) (g : (↑G.toPrelaxFunctor).obj b ⟶ a') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (θ.app b) g).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality θ f) g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑F.toPrelaxFunctor).map f) (η.app b) g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) g) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) ((↑G.toPrelaxFunctor).map f)) g))

@[simp]

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

def CategoryTheory.OplaxNatTrans.Modification.vcomp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} {ι : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification η θ) (Δ : CategoryTheory.OplaxNatTrans.Modification θ ι) : CategoryTheory.OplaxNatTrans.Modification η ι

Vertical composition of modifications.

@[simp]

theorem CategoryTheory.OplaxNatTrans.category_id {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) (η : F ⟶ G) : CategoryTheory.CategoryStruct.id η = CategoryTheory.OplaxNatTrans.Modification.id η

@[simp]

theorem CategoryTheory.OplaxNatTrans.category_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) : ∀ {X Y Z : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification X Y) (Δ : CategoryTheory.OplaxNatTrans.Modification Y Z), CategoryTheory.CategoryStruct.comp Γ Δ = CategoryTheory.OplaxNatTrans.Modification.vcomp Γ Δ

instance CategoryTheory.OplaxNatTrans.category {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) : CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)

Category structure on the oplax natural transformations between OplaxFunctors.

theorem CategoryTheory.OplaxNatTrans.ext {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F ⟶ G} {β : F ⟶ G} {m : α ⟶ β} {n : α ⟶ β} (w : ∀ (b : B), m.app b = n.app b) : m = n

@[simp]

theorem CategoryTheory.OplaxNatTrans.Modification.id_app' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {X : B} {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (α : F ⟶ G) : (CategoryTheory.CategoryStruct.id α).app X = CategoryTheory.CategoryStruct.id (α.app X)

@[simp]

theorem CategoryTheory.OplaxNatTrans.Modification.comp_app' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {X : B} {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F ⟶ G} {β : F ⟶ G} {γ : F ⟶ G} (m : α ⟶ β) (n : β ⟶ γ) : (CategoryTheory.CategoryStruct.comp m n).app X = CategoryTheory.CategoryStruct.comp (m.app X) (n.app X)

@[simp]

theorem CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (app b).hom) (CategoryTheory.OplaxNatTrans.naturality θ f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality η f) (CategoryTheory.Bicategory.whiskerRight (app a).hom ((↑G.toPrelaxFunctor).map f))) (a : B) : (CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).hom.app a = (app a).hom

@[simp]

theorem CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (app b).hom) (CategoryTheory.OplaxNatTrans.naturality θ f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality η f) (CategoryTheory.Bicategory.whiskerRight (app a).hom ((↑G.toPrelaxFunctor).map f))) (a : B) : (CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).inv.app a = (app a).inv

def CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑F.toPrelaxFunctor).map f) (app b).hom) (CategoryTheory.OplaxNatTrans.naturality θ f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxNatTrans.naturality η f) (CategoryTheory.Bicategory.whiskerRight (app a).hom ((↑G.toPrelaxFunctor).map f))) : η ≅ θ

Construct a modification isomorphism between oplax natural transformations by giving object level isomorphisms, and checking naturality only in the forward direction.