Theorems · Theorem · category theory

CategoryTheory.Lax.LaxTrans.comp_naturality

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

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory