{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        {C₇ : Type u₇} →
                          {C₈ : Type u₈} →
                            [inst_4 : CategoryTheory.Category.{v₇, u₇} C₇] →
                              [inst_5 : CategoryTheory.Category.{v₈, u₈} C₈] →
                                {L' : CategoryTheory.Functor C₃ C₇} →
                                  {R'' : CategoryTheory.Functor C₄ C₈} →
                                    {B'' : CategoryTheory.Functor C₇ C₈} →
                                      CategoryTheory.TwoSquare T L R B →
                                        CategoryTheory.TwoSquare B L' R'' B'' →
                                          CategoryTheory.TwoSquare T (L.comp L') (R.comp R'') B''