Theorems · Theorem · category theory

CategoryTheory.Oplax.OplaxTrans.naturality_comp

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

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Cited by

3 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory