Theorems · Theorem · category theory

CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app

∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (η : CategoryTheory.Oplax.StrongTrans F G) {a : B} {a' : CategoryTheory.Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (f.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X))
      (f.toFunctor.map ((G.mapId a).toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (f.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app a).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X))))
        (f.toFunctor.map (CategoryTheory.CategoryStruct.id ((η.app a).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