Theorems · Theorem · category theory

CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc

∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
          h_1))

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Lax

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory