Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app

∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (η : F ⟶ G) {a b c : B} {a' : CategoryTheory.Cat} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (h.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom.toNatTrans.app X))
      (h.toFunctor.map ((G.mapComp f g).hom.toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp
      (h.toFunctor.map ((η.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (h.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app c).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)))))
        (CategoryTheory.CategoryStruct.comp
          (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X)))
          (CategoryTheory.CategoryStruct.comp
            (h.toFunctor.map
              (CategoryTheory.CategoryStruct.id
                ((G.map g).toFunctor.obj ((η.app b).toFunctor.obj ((F.map f).toFunctor.obj X)))))
            (CategoryTheory.CategoryStruct.comp
              (h.toFunctor.map ((G.map g).toFunctor.map ((η.naturality f).hom.toNatTrans.app X)))
              (h.toFunctor.map
                (CategoryTheory.CategoryStruct.id
                  ((G.map g).toFunctor.obj ((G.map f).toFunctor.obj ((η.app a).toFunctor.obj X)))))))))

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory