Theorems · Theorem · category theory

CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app

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

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory