Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom

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

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Cited by

3 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory