Theorems · Theorem · category theory

CategoryTheory.Lax.StrongTrans.vComp_naturality_hom

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G)
  (θ : CategoryTheory.Lax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((η.vComp θ).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.app b))
            (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).hom)))

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory