Theorems · Theorem · category theory

CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app

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