mathlib documentation

category_theory.bicategory.functor_bicategory

The bicategory of oplax functors between two bicategories #

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

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
@[simp]
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
@[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) :
@[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) :
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

Left unitor for the vertical composition of oplax natural transformations.

Equations

Right unitor for the vertical composition of oplax natural transformations.

Equations
@[protected, instance]

A bicategory structure on the oplax functors between bicategories.

Equations