∀ {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).hom.app X).2.2 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inr_ A' T).whiskerLeft
        ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).inv)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Sum.inr_ A' T).associator
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).inv
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inrCompInrCompInverseAssociator A A' T).hom X))