Theorems · Theorem · category theory

CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst

∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inr_ A A').associator (CategoryTheory.Sum.inl_ (A ⊕ A') T) X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inlCompInrCompInverseAssociator A A' T).inv X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Sum.inl_ A' T).associator
              ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).hom
          ((CategoryTheory.Sum.inl_ A' T).whiskerLeft
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).hom)))

Defined in

Mathlib.CategoryTheory.Sums.Products

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category