Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

Oplax functoriality.

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory