Transformations between lax functors

Just as there are natural transformations between functors, there are transformations between lax functors. The equality in the naturality condition of a natural transformation gets replaced by a specified 2-morphism. Now, there are three possible types of transformations (between lax functors):

• Lax natural transformations;
• OpLax natural transformations;
• Strong natural transformations. These differ in the direction (and invertibility) of the 2-morphisms involved in the naturality condition.

Main definitions

• Lax.LaxTrans F G: lax transformations between lax functors F and G. The naturality condition is given by a 2-morphism app a ≫ G.map f ⟶ F.map f ≫ app b for each 1-morphism f : a ⟶ b.
• Lax.OplaxTrans F G: oplax transformations between lax functors F and G. The naturality condition is given by a 2-morphism F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
• Lax.StrongTrans F G: Strong transformations between lax functors F and G. The naturality condition is given by a 2-morphism app a ≫ G.map f ≅ F.map f ≫ app b for each 1-morphism f : a ⟶ b.

Using these, we define three CategoryStruct (scoped) instances on B ⥤ᴸ C, in the Lax.LaxTrans, Lax.Oplax, and Lax.StrongTrans namespaces. The arrows in these CategoryStruct's are given by lax transformations, oplax transformations, and strong transformations respectively.

We also provide API for going between lax transformations and strong transformations:

• Lax.StrongCore F G: a structure on a lax transformation between lax functors that promotes it to a strong transformation.
• Lax.mkOfLax η η': given a lax transformation η such that each component 2-morphism is an isomorphism, mkOfLax gives the corresponding strong transformation.

References

• Niles Johnson, Donald Yau, 2-Dimensional Categories, section 4.2.

structure CategoryTheory.Lax.LaxTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : LaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

If η is a lax 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 : app a ≫ G.map f ⟶ F.map f ≫ app b for each 1-morphism f : a ⟶ b. These 2-morphisms 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

  The component 1-morphisms of a lax transformation.

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

  The 2-morphisms underlying the lax naturality constraint.

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

  Naturality of the lax naturality constraint.

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

  Lax unity.

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

  Lax functoriality.

@[simp]

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

Naturality of the lax naturality constraint.

@[simp]

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

Lax functoriality.

@[simp]

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

Lax unity.

def CategoryTheory.Lax.LaxTrans.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) : LaxTrans F F

The identity lax transformation.

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

@[reducible, inline]

abbrev CategoryTheory.Lax.LaxTrans.vCompApp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) (a : B) : F.obj a ⟶ H.obj a

Auxiliary definition for vComp.

@[reducible, inline]

abbrev CategoryTheory.Lax.LaxTrans.vCompNaturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b : B} (f : a ⟶ b) : CategoryStruct.comp (CategoryStruct.comp (η.app a) (θ.app a)) (H.map f) ⟶ CategoryStruct.comp (F.map f) (CategoryStruct.comp (η.app b) (θ.app b))

Auxiliary definition for vComp.

theorem CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b : B} {f g : a ⟶ b} (β : f ⟶ g) : CategoryStruct.comp (η.vCompNaturality θ f) (Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b)) = CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β)) (η.vCompNaturality θ g)

theorem CategoryTheory.Lax.LaxTrans.vComp_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) (a : B) : CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a)) (η.vCompNaturality θ (CategoryStruct.id a)) = CategoryStruct.comp (Bicategory.rightUnitor (η.vCompApp θ a)).hom (CategoryStruct.comp (Bicategory.leftUnitor (η.vCompApp θ a)).inv (Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a)))

theorem CategoryTheory.Lax.LaxTrans.vComp_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g)) (η.vCompNaturality θ (CategoryStruct.comp f g)) = CategoryStruct.comp (Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).inv (Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c))))))

def CategoryTheory.Lax.LaxTrans.vComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) : LaxTrans F H

Vertical composition of lax transformations.

@[simp]

theorem CategoryTheory.Lax.LaxTrans.vComp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) (a : B) : (η.vComp θ).app a = η.vCompApp θ a

@[simp]

theorem CategoryTheory.Lax.LaxTrans.vComp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : LaxTrans F G) (θ : LaxTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (η.vComp θ).naturality f = η.vCompNaturality θ f

def CategoryTheory.Lax.LaxTrans.instCategoryStructLaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (LaxFunctor B C)

CategoryStruct on B ⥤ᴸ C where the (1-)morphisms are given by lax transformations.

@[simp]

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

@[simp]

theorem CategoryTheory.Lax.LaxTrans.comp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : LaxTrans X✝ Y✝) (θ : LaxTrans Y✝ Z✝) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.comp η θ).naturality f = η.vCompNaturality θ f

@[simp]

theorem CategoryTheory.Lax.LaxTrans.comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : LaxTrans X✝ Y✝) (θ : LaxTrans Y✝ Z✝) (a : B) : (CategoryStruct.comp η θ).app a = η.vCompApp θ a

@[simp]

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

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

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

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

  The component 1-morphisms of an oplax transformation.

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

  The 2-morphisms underlying the oplax naturality constraint.

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

  Naturality of the oplax naturality constraint.

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

@[simp]

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

@[simp]

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

@[simp]

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

Naturality of the oplax naturality constraint.

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

The identity oplax transformation.

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

@[reducible, inline]

abbrev CategoryTheory.Lax.OplaxTrans.vCompApp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) (a : B) : F.obj a ⟶ H.obj a

Auxiliary definition for vComp.

@[reducible, inline]

abbrev CategoryTheory.Lax.OplaxTrans.vCompNaturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) {a b : B} (f : a ⟶ b) : CategoryStruct.comp (F.map f) (CategoryStruct.comp (η.app b) (θ.app b)) ⟶ CategoryStruct.comp (CategoryStruct.comp (η.app a) (θ.app a)) (H.map f)

Auxiliary definition for vComp.

theorem CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) {a b : B} {f g : a ⟶ b} (β : f ⟶ g) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b)) (η.vCompNaturality θ g) = CategoryStruct.comp (η.vCompNaturality θ f) (Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β))

theorem CategoryTheory.Lax.OplaxTrans.vComp_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) (a : B) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a)) (η.vCompNaturality θ (CategoryStruct.id a)) = CategoryStruct.comp (Bicategory.leftUnitor (η.vCompApp θ a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (η.vCompApp θ a)).inv (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a)))

theorem CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c)) (η.vCompNaturality θ (CategoryStruct.comp f g)) = CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g)) (CategoryStruct.comp (Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).hom (Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g))))))

def CategoryTheory.Lax.OplaxTrans.vComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : OplaxTrans F G) (θ : OplaxTrans G H) : OplaxTrans F H

Vertical composition of oplax transformations.

def CategoryTheory.Lax.OplaxTrans.instCategoryStructLaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (LaxFunctor B C)

CategoryStruct on B ⥤ᴸ C where the (1-)morphisms are given by oplax transformations.

@[simp]

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

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) (a : B) : (CategoryStruct.comp η θ).app a = η.vCompApp θ a

@[simp]

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

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.comp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : OplaxTrans X✝ Y✝) (θ : OplaxTrans Y✝ Z✝) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.comp η θ).naturality f = η.vCompNaturality θ f

structure CategoryTheory.Lax.StrongTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : LaxFunctor B C) : Type (max (max (max u₁ v₁) v₂) w₂)

A strong natural transformation between lax 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 : app a ≫ G.map f ≅ F.map f ≫ app b 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) : CategoryStruct.comp (self.app a) (G.map f) ≅ CategoryStruct.comp (F.map f) (self.app b)
• naturality_naturality {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : CategoryStruct.comp (self.naturality f).hom (Bicategory.whiskerRight (F.map₂ η) (self.app b)) = CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.map₂ η)) (self.naturality g).hom
• naturality_id (a : B) : CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapId a)) (self.naturality (CategoryStruct.id a)).hom = CategoryStruct.comp (Bicategory.rightUnitor (self.app a)).hom (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).inv (Bicategory.whiskerRight (F.mapId a) (self.app a)))

  Lax unity.

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

  Lax functoriality.

@[simp]

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

Lax functoriality.

@[simp]

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

@[simp]

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

Lax unity.

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

A structure on a lax transformation that promotes it to a strong transformation.

See Pseudofunctor.StrongTrans.mkOfLax.

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

  The underlying 2-isomorphisms of the naturality constraint.

• naturality_hom {a b : B} (f : a ⟶ b) : (self.naturality f).hom = η.naturality f

  The 2-isomorphisms agree with the underlying 2-morphism of the lax transformation.

def CategoryTheory.Lax.StrongTrans.toLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : StrongTrans F G) : LaxTrans F G

The underlying lax natural transformation of a strong natural transformation.

@[simp]

theorem CategoryTheory.Lax.StrongTrans.toLax_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : StrongTrans F G) (a : B) : η.toLax.app a = η.app a

@[simp]

theorem CategoryTheory.Lax.StrongTrans.toLax_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : StrongTrans F G) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : η.toLax.naturality f = (η.naturality f).hom

def CategoryTheory.Lax.StrongTrans.mkOfLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : LaxTrans F G) (η' : LaxTrans.StrongCore η) : StrongTrans F G

Construct a strong natural transformation from a lax natural transformation whose naturality 2-morphism is an isomorphism.

noncomputable def CategoryTheory.Lax.StrongTrans.mkOfLax' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : LaxTrans F G) [∀ (a b : B) (f : a ⟶ b), IsIso (η.naturality f)] : StrongTrans F G

Construct a strong natural transformation from a lax natural transformation whose naturality 2-morphism is an isomorphism.

def CategoryTheory.Lax.StrongTrans.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) : StrongTrans F F

The identity strong natural transformation.

@[simp]

theorem CategoryTheory.Lax.StrongTrans.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (a : B) : (id F).app a = (LaxTrans.id F).app a

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Lax.StrongTrans.id.toLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) : (id F).toLax = LaxTrans.id F

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

def CategoryTheory.Lax.StrongTrans.vComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) : StrongTrans F H

Vertical composition of strong natural transformations.

@[simp]

theorem CategoryTheory.Lax.StrongTrans.vComp_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((η.vComp θ).naturality f).hom = CategoryStruct.comp (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).hom) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom (θ.app b✝)) (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).hom)))

@[simp]

theorem CategoryTheory.Lax.StrongTrans.vComp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) (a : B) : (η.vComp θ).app a = η.toLax.vCompApp θ.toLax a

@[simp]

theorem CategoryTheory.Lax.StrongTrans.vComp_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : StrongTrans F G) (θ : StrongTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : ((η.vComp θ).naturality f).inv = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).inv (θ.app b✝)) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).inv) (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).inv)))

def CategoryTheory.Lax.StrongTrans.categoryStruct {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (LaxFunctor B C)

CategoryStruct on B ⥤ᴸ C where the (1-)morphisms are given by strong transformations.

@[simp]

theorem CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : StrongTrans X✝ Y✝) (θ : StrongTrans Y✝ Z✝) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.comp η θ).naturality f = Bicategory.associator (η.app a✝) (θ.app a✝) (Z✝.map f) ≪≫ Bicategory.whiskerLeftIso (η.app a✝) (θ.naturality f) ≪≫ (Bicategory.associator (η.app a✝) (Y✝.map f) (θ.app b✝)).symm ≪≫ Bicategory.whiskerRightIso (η.naturality f) (θ.app b✝) ≪≫ Bicategory.associator (X✝.map f) (η.app b✝) (θ.app b✝)

@[simp]

theorem CategoryTheory.Lax.StrongTrans.categoryStruct_comp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {X✝ Y✝ Z✝ : LaxFunctor B C} (η : StrongTrans X✝ Y✝) (θ : StrongTrans Y✝ Z✝) (a : B) : (CategoryStruct.comp η θ).app a = η.toLax.vCompApp θ.toLax a

@[simp]

theorem CategoryTheory.Lax.StrongTrans.categoryStruct_id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (a : B) : (CategoryStruct.id F).app a = (LaxTrans.id F).app a

@[simp]

theorem CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) : (CategoryStruct.id F).naturality f = Bicategory.leftUnitor (F.map f) ≪≫ (Bicategory.rightUnitor (F.map f)).symm