Strong natural transformations

A strong natural transformation is an oplax natural transformation such that each component 2-cell is an isomorphism.

Main definitions

• StrongOplaxNatTrans F G : strong natural transformations between oplax functors F and G.
• mkOfOplax η η' : given an oplax natural transformation η such that each component 2-cell is an isomorphism, mkOfOplax gives the corresponding strong natural transformation.
• StrongOplaxNatTrans.vcomp η θ : the vertical composition of strong natural transformations η and θ.
• StrongOplaxNatTrans.category F G : a category structure on pseudofunctors between F and G, where the morphisms are strong natural transformations.

TODO

After having defined lax functors, we should define 3 different types of strong natural transformations:

• strong natural transformations between oplax functors (as defined here).
• strong natural transformations between lax functors.
• strong natural transformations between pseudofunctors. From these types of strong natural transformations, we can define the underlying natural transformations between the underlying oplax resp. lax functors. Many properties can then be inferred from these.

References

• Niles Johnson, Donald Yau, 2-Dimensional Categories

structure CategoryTheory.StrongOplaxNatTrans {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₂)

A strong natural transformation between oplax functors F and G is a natural transformation that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:

• a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B.
• a 2-isomorphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
• These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

• app : (a : B) → F.obj a ⟶ G.obj a
• naturality : {a b : B} → (f : a ⟶ b) → 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).hom = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
• naturality_id : ∀ (a : B), CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom (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)).hom (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).hom) (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).hom (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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).hom = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans F G) (a : B) : CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans F G) {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom (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).hom) (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).hom (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom (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).hom) (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).hom (G.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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).hom h) = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom (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))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.toOplax_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.StrongOplaxNatTrans F G) : ∀ {a b : B} (f : a ⟶ b), η.toOplax.naturality f = (η.naturality f).hom

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.toOplax_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.StrongOplaxNatTrans F G) (a : B) : η.toOplax.app a = η.app a

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

The underlying oplax natural transformation of a strong natural transformation.

Equations

• η.toOplax = { app := η.app, naturality := fun {a b : B} (f : a ⟶ b) => (η.naturality f).hom, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

def CategoryTheory.StrongOplaxNatTrans.mkOfOplax {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) (η' : η.StrongCore) : CategoryTheory.StrongOplaxNatTrans F G

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

Equations

• CategoryTheory.StrongOplaxNatTrans.mkOfOplax η η' = { app := η.app, naturality := fun {a b : B} => η'.naturality, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

noncomputable def CategoryTheory.StrongOplaxNatTrans.mkOfOplax' {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) (f : a ⟶ b), CategoryTheory.IsIso (η.naturality f)] : CategoryTheory.StrongOplaxNatTrans F G

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id_naturality_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : ∀ {a b : B} (f : a ⟶ b), ((CategoryTheory.StrongOplaxNatTrans.id F).naturality f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id_naturality_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : ∀ {a b : B} (f : a ⟶ b), ((CategoryTheory.StrongOplaxNatTrans.id F).naturality f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv

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

The identity strong natural transformation.

Equations

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

@[simp]

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

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

Equations

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

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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✝).hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h)

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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).hom h✝) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom 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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom 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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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✝)).hom) (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✝).hom)) (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).hom (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom) (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).hom)) (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).hom (H.map h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom 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).hom 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).hom (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom 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).hom 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).hom (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom) (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom) (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.StrongOplaxNatTrans.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.StrongOplaxNatTrans 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)).hom 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)))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom 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.StrongOplaxNatTrans.vcomp_naturality_inv {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.StrongOplaxNatTrans F G) (θ : CategoryTheory.StrongOplaxNatTrans G H) : ∀ {a b : B} (f : a ⟶ b), ((η.vcomp θ).naturality f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).inv (θ.app b)) (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).hom)))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.vcomp_naturality_hom {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.StrongOplaxNatTrans F G) (θ : CategoryTheory.StrongOplaxNatTrans G H) : ∀ {a b : B} (f : a ⟶ b), ((η.vcomp θ).naturality f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.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).hom) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).inv)))

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans F G) (θ : CategoryTheory.StrongOplaxNatTrans G H) (a : B) : (η.vcomp θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)

def CategoryTheory.StrongOplaxNatTrans.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.StrongOplaxNatTrans F G) (θ : CategoryTheory.StrongOplaxNatTrans G H) : CategoryTheory.StrongOplaxNatTrans F H

Vertical composition of strong natural transformations.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.categoryStruct_id (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : CategoryTheory.CategoryStruct.id F = CategoryTheory.StrongOplaxNatTrans.id F.toOplax

instance CategoryTheory.Pseudofunctor.categoryStruct (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.Pseudofunctor B C)

Equations

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