Theorems · Theorem · category theory

CategoryTheory.Lax.StrongTrans.naturality_comp_assoc

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) (self.app c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
                h)))))

Lax functoriality.

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses Quot.sound

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory