Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

The bicategory of oplax functors between two bicategories #

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

Left whiskering of an oplax natural transformation and a modification.

Equations
Instances For

    Right whiskering of an oplax natural transformation and a modification.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.OplaxFunctor.bicategory_whiskerRight_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] :
      ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 x_4 : x x_1) (Γ : x_3 x_4) (η : x_1 x_2) (a : B), (CategoryTheory.Bicategory.whiskerRight Γ η).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (η.app a)
      @[simp]
      theorem CategoryTheory.OplaxFunctor.bicategory_whiskerLeft_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] :
      ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (η : x x_1) (x_3 x_4 : x_1 x_2) (Γ : x_3 x_4) (a : B), (CategoryTheory.Bicategory.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)
      @[simp]
      theorem CategoryTheory.OplaxFunctor.bicategory_associator_inv_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] :
      ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x x_1) (θ : x_1 x_2) (ι : x_2 x_3) (a : B), (CategoryTheory.Bicategory.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
      @[simp]
      theorem CategoryTheory.OplaxFunctor.bicategory_associator_hom_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] :
      ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x x_1) (θ : x_1 x_2) (ι : x_2 x_3) (a : B), (CategoryTheory.Bicategory.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

      A bicategory structure on the oplax functors between bicategories.

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