category_theory.bicategory.functor_bicategory

source

def category_theory.oplax_nat_trans.whisker_left {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) :

η ≫ θ ⟶ η ≫ ι

Left whiskering of an oplax natural transformation and a modification.

Equations

category_theory.oplax_nat_trans.whisker_left η Γ = {app := λ (a : B), category_theory.bicategory.whisker_left (η.app a) (Γ.app a), naturality' := _}

source

@[simp]

theorem category_theory.oplax_nat_trans.whisker_left_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) :

(category_theory.oplax_nat_trans.whisker_left η Γ).app a = category_theory.bicategory.whisker_left (η.app a) (Γ.app a)

source

def category_theory.oplax_nat_trans.whisker_right {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) :

η ≫ ι ⟶ θ ≫ ι

Right whiskering of an oplax natural transformation and a modification.

Equations

category_theory.oplax_nat_trans.whisker_right Γ ι = {app := λ (a : B), category_theory.bicategory.whisker_right (Γ.app a) (ι.app a), naturality' := _}

source

@[simp]

theorem category_theory.oplax_nat_trans.whisker_right_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) :

(category_theory.oplax_nat_trans.whisker_right Γ ι).app a = category_theory.bicategory.whisker_right (Γ.app a) (ι.app a)

source

@[simp]

theorem category_theory.oplax_nat_trans.associator_inv_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H I : category_theory.oplax_functor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(category_theory.oplax_nat_trans.associator η θ ι).inv.app a = (category_theory.bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

@[simp]

theorem category_theory.oplax_nat_trans.associator_hom_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H I : category_theory.oplax_functor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(category_theory.oplax_nat_trans.associator η θ ι).hom.app a = (category_theory.bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

def category_theory.oplax_nat_trans.associator {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H I : category_theory.oplax_functor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :

(η ≫ θ) ≫ ι ≅ η ≫ θ ≫ ι

Associator for the vertical composition of oplax natural transformations.

Equations

category_theory.oplax_nat_trans.associator η θ ι = category_theory.oplax_nat_trans.modification_iso.of_components (λ (a : B), category_theory.bicategory.associator (η.app a) (θ.app a) (ι.app a)) _

source

@[simp]

theorem category_theory.oplax_nat_trans.left_unitor_hom_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) (a : B) :

(category_theory.oplax_nat_trans.left_unitor η).hom.app a = (category_theory.bicategory.left_unitor (η.app a)).hom

source

@[simp]

theorem category_theory.oplax_nat_trans.left_unitor_inv_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) (a : B) :

(category_theory.oplax_nat_trans.left_unitor η).inv.app a = (category_theory.bicategory.left_unitor (η.app a)).inv

source

def category_theory.oplax_nat_trans.left_unitor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) :

𝟙 F ≫ η ≅ η

Left unitor for the vertical composition of oplax natural transformations.

Equations

category_theory.oplax_nat_trans.left_unitor η = category_theory.oplax_nat_trans.modification_iso.of_components (λ (a : B), category_theory.bicategory.left_unitor (η.app a)) _

source

@[simp]

theorem category_theory.oplax_nat_trans.right_unitor_inv_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) (a : B) :

(category_theory.oplax_nat_trans.right_unitor η).inv.app a = (category_theory.bicategory.right_unitor (η.app a)).inv

source

@[simp]

theorem category_theory.oplax_nat_trans.right_unitor_hom_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) (a : B) :

(category_theory.oplax_nat_trans.right_unitor η).hom.app a = (category_theory.bicategory.right_unitor (η.app a)).hom

source

def category_theory.oplax_nat_trans.right_unitor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) :

η ≫ 𝟙 G ≅ η

Right unitor for the vertical composition of oplax natural transformations.

Equations

category_theory.oplax_nat_trans.right_unitor η = category_theory.oplax_nat_trans.modification_iso.of_components (λ (a : B), category_theory.bicategory.right_unitor (η.app a)) _

source

@[simp]

theorem category_theory.oplax_functor.bicategory_right_unitor (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) (η : F ⟶ G) :

category_theory.bicategory.right_unitor η = category_theory.oplax_nat_trans.right_unitor η

source

@[simp]

theorem category_theory.oplax_functor.bicategory_hom_category (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F H : category_theory.oplax_functor B C) :

category_theory.bicategory.hom_category F H = category_theory.oplax_nat_trans.category F H

source

@[simp]

theorem category_theory.oplax_functor.bicategory_associator (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G H I : category_theory.oplax_functor B C) (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :

category_theory.bicategory.associator η θ ι = category_theory.oplax_nat_trans.associator η θ ι

source

@[simp]

theorem category_theory.oplax_functor.bicategory_whisker_left (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G H : category_theory.oplax_functor B C) (η : F ⟶ G) (_x _x_1 : G ⟶ H) (Γ : _x ⟶ _x_1) :

category_theory.bicategory.whisker_left η Γ = category_theory.oplax_nat_trans.whisker_left η Γ

source

@[simp]

theorem category_theory.oplax_functor.bicategory_left_unitor (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) (η : F ⟶ G) :

category_theory.bicategory.left_unitor η = category_theory.oplax_nat_trans.left_unitor η

source

@[simp]

theorem category_theory.oplax_functor.bicategory_whisker_right (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G H : category_theory.oplax_functor B C) (_x _x_1 : F ⟶ G) (Γ : _x ⟶ _x_1) (η : G ⟶ H) :

category_theory.bicategory.whisker_right Γ η = category_theory.oplax_nat_trans.whisker_right Γ η

source

@[protected, instance]

def category_theory.oplax_functor.bicategory (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] :

category_theory.bicategory (category_theory.oplax_functor B C)

A bicategory structure on the oplax functors between bicategories.

Equations

category_theory.oplax_functor.bicategory B C = {to_category_struct := category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct B C _inst_2, hom_category := λ (F H : category_theory.oplax_functor B C), category_theory.oplax_nat_trans.category F H, whisker_left := λ (F G H : category_theory.oplax_functor B C) (η : F ⟶ G) (_x _x_1 : G ⟶ H) (Γ : _x ⟶ _x_1), category_theory.oplax_nat_trans.whisker_left η Γ, whisker_right := λ (F G H : category_theory.oplax_functor B C) (_x _x_1 : F ⟶ G) (Γ : _x ⟶ _x_1) (η : G ⟶ H), category_theory.oplax_nat_trans.whisker_right Γ η, associator := λ (F G H I : category_theory.oplax_functor B C), category_theory.oplax_nat_trans.associator, left_unitor := λ (F G : category_theory.oplax_functor B C), category_theory.oplax_nat_trans.left_unitor, right_unitor := λ (F G : category_theory.oplax_functor B C), category_theory.oplax_nat_trans.right_unitor, whisker_left_id' := _, whisker_left_comp' := _, id_whisker_left' := _, comp_whisker_left' := _, id_whisker_right' := _, comp_whisker_right' := _, whisker_right_id' := _, whisker_right_comp' := _, whisker_assoc' := _, whisker_exchange' := _, pentagon' := _, triangle' := _}

source

@[simp]

theorem category_theory.oplax_functor.bicategory_to_category_struct (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] :

category_theory.bicategory.to_category_struct = category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct B C

mathlib3 documentation

The bicategory of oplax functors between two bicategories #