The bicategory of pseudofunctors

Given bicategories B and C, we define a bicategory structure on Pseudofunctor B C whose

• objects are pseudofunctors,
• 1-morphisms are strong natural transformations, and
• 2-morphisms are modifications.

We scope this instance to the CategoryTheory.Pseudofunctor.StrongTrans namespace to avoid potential future conflicts with other bicategory instances on Pseudofunctor B C.

@[reducible, inline]

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

Left whiskering of a strong natural transformation between pseudofunctors and a modification.

Equations

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

@[reducible, inline]

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

Right whiskering of an strong natural transformation between pseudofunctors and a modification.

Equations

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

@[reducible, inline]

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

Associator for the vertical composition of strong natural transformations between pseudofunctors.

Equations

• CategoryTheory.Pseudofunctor.StrongTrans.associator η θ ι = CategoryTheory.Pseudofunctor.StrongTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)) ⋯

@[reducible, inline]

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

Left unitor for the vertical composition of strong natural transformations between pseudofunctors.

Equations

• CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor η = CategoryTheory.Pseudofunctor.StrongTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.leftUnitor (η.app a)) ⋯

@[reducible, inline]

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

Right unitor for the vertical composition of strong natural transformations between pseudofunctors.

Equations

• CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor η = CategoryTheory.Pseudofunctor.StrongTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.rightUnitor (η.app a)) ⋯

def CategoryTheory.Pseudofunctor.StrongTrans.instBicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] : Bicategory (Pseudofunctor B C)

A bicategory structure on pseudofunctors, with strong transformations as 1-morphisms.

Note that this instance is scoped to the Pseudofunctor.StrongTrans namespace.

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G H : Pseudofunctor B C} (η : F ⟶ G) (x✝ x✝¹ : G ⟶ H) (Γ : x✝ ⟶ x✝¹) (a : B) : (Bicategory.whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G H : Pseudofunctor B C} (x✝ x✝¹ : F ⟶ G) (Γ : x✝ ⟶ x✝¹) (η : G ⟶ H) (a : B) : (Bicategory.whiskerRight Γ η).as.app a = Bicategory.whiskerRight (Γ.as.app a) (η.app a)

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) (a : B) : (Bicategory.rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) (a : B) : (Bicategory.leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) (a : B) : (Bicategory.rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) (a : B) : (Bicategory.leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom