The bicategory of oplax functors between two bicategories

Given bicategories B and C, we give a bicategory structure on OplaxFunctor B C whose

• objects are oplax functors,
• 1-morphisms are oplax natural transformations, and
• 2-morphisms are modifications.

def CategoryTheory.OplaxNatTrans.whiskerLeft {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : CategoryStruct.comp η θ ⟶ CategoryStruct.comp η ι

Left whiskering of an oplax natural transformation and a modification.

Equations

• CategoryTheory.OplaxNatTrans.whiskerLeft η Γ = { app := fun (a : B) => CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.OplaxNatTrans.whiskerLeft_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) : (whiskerLeft η Γ).app a = Bicategory.whiskerLeft (η.app a) (Γ.app a)

def CategoryTheory.OplaxNatTrans.whiskerRight {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : CategoryStruct.comp η ι ⟶ CategoryStruct.comp θ ι

Right whiskering of an oplax natural transformation and a modification.

Equations

• CategoryTheory.OplaxNatTrans.whiskerRight Γ ι = { app := fun (a : B) => CategoryTheory.Bicategory.whiskerRight (Γ.app a) (ι.app a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.OplaxNatTrans.whiskerRight_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) : (whiskerRight Γ ι).app a = Bicategory.whiskerRight (Γ.app a) (ι.app a)

def CategoryTheory.OplaxNatTrans.associator {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : CategoryStruct.comp (CategoryStruct.comp η θ) ι ≅ CategoryStruct.comp η (CategoryStruct.comp θ ι)

Associator for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.associator η θ ι = CategoryTheory.Oplax.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxNatTrans.associator_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) : (associator η θ ι).inv.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

@[simp]

theorem CategoryTheory.OplaxNatTrans.associator_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) : (associator η θ ι).hom.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

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

Left unitor for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.leftUnitor η = CategoryTheory.Oplax.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.leftUnitor (η.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxNatTrans.leftUnitor_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) : (leftUnitor η).hom.app a = (Bicategory.leftUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxNatTrans.leftUnitor_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) : (leftUnitor η).inv.app a = (Bicategory.leftUnitor (η.app a)).inv

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

Right unitor for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.rightUnitor η = CategoryTheory.Oplax.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.rightUnitor (η.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxNatTrans.rightUnitor_inv_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) : (rightUnitor η).inv.app a = (Bicategory.rightUnitor (η.app a)).inv

@[simp]

theorem CategoryTheory.OplaxNatTrans.rightUnitor_hom_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) (a : B) : (rightUnitor η).hom.app a = (Bicategory.rightUnitor (η.app a)).hom

instance CategoryTheory.OplaxFunctor.bicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] : Bicategory (OplaxFunctor B C)

A bicategory structure on the oplax functors between bicategories.

Equations

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

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_homCategory_comp_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a b : OplaxFunctor B C) {X✝ Y✝ Z✝ : a ⟶ b} (Γ : Oplax.Modification X✝ Y✝) (Δ : Oplax.Modification Y✝ Z✝) (a✝ : B) : (CategoryStruct.comp Γ Δ).app a✝ = CategoryStruct.comp (Γ.app a✝) (Δ.app a✝)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_id_naturality (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F : OplaxFunctor 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.OplaxFunctor.bicategory_associator_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) : (Bicategory.associator η θ ι).inv.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_whiskerLeft_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (x✝³ x✝⁴ : x✝¹ ⟶ x✝²) (Γ : x✝³ ⟶ x✝⁴) (a : B) : (Bicategory.whiskerLeft η Γ).app a = Bicategory.whiskerLeft (η.app a) (Γ.app a)

@[simp]

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

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_leftUnitor_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) : (Bicategory.leftUnitor η).inv.app a = (Bicategory.leftUnitor (η.app a)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_rightUnitor_inv_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) : (Bicategory.rightUnitor η).inv.app a = (Bicategory.rightUnitor (η.app a)).inv

@[simp]

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

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_leftUnitor_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) : (Bicategory.leftUnitor η).hom.app a = (Bicategory.leftUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_associator_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ : OplaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) : (Bicategory.associator η θ ι).hom.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_Hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F G : OplaxFunctor B C) : (F ⟶ G) = OplaxNatTrans F G

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_rightUnitor_hom_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : OplaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) : (Bicategory.rightUnitor η).hom.app a = (Bicategory.rightUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_comp_naturality (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : OplaxFunctor B C} (η : OplaxNatTrans X✝ Y✝) (θ : OplaxNatTrans Y✝ Z✝) {a b : B} (f : a ⟶ b) : (CategoryStruct.comp η θ).naturality f = CategoryStruct.comp (Bicategory.associator (X✝.map f) (η.app b) (θ.app b)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) (θ.app b)) (CategoryStruct.comp (Bicategory.associator (η.app a) (Y✝.map f) (θ.app b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (Bicategory.associator (η.app a) (θ.app a) (Z✝.map f)).inv)))

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_homCategory_id_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a b : OplaxFunctor B C) (η : a ⟶ b) (a✝ : B) : (CategoryStruct.id η).app a✝ = CategoryStruct.id (η.app a✝)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_whiskerRight_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : OplaxFunctor B C} (x✝³ x✝⁴ : x✝ ⟶ x✝¹) (Γ : x✝³ ⟶ x✝⁴) (η : x✝¹ ⟶ x✝²) (a : B) : (Bicategory.whiskerRight Γ η).app a = Bicategory.whiskerRight (Γ.app a) (η.app a)