{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f x y z : B} →
      {g₁ : a ⟶ d} →
        {h₁ : b ⟶ e} →
          {k₁ : c ⟶ f} →
            {g₂ : d ⟶ x} →
              {h₂ : e ⟶ y} →
                {k₂ : f ⟶ z} →
                  {l₁ : a ⟶ b} →
                    {l₂ : b ⟶ c} →
                      {l₃ : d ⟶ e} →
                        {l₄ : e ⟶ f} →
                          {l₅ : x ⟶ y} →
                            {l₆ : y ⟶ z} →
                              (CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁) →
                                (CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁) →
                                  (CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶
                                      CategoryTheory.CategoryStruct.comp l₃ h₂) →
                                    (CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶
                                        CategoryTheory.CategoryStruct.comp l₄ k₂) →
                                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₁ g₂)
                                          (CategoryTheory.CategoryStruct.comp l₅ l₆) ⟶
                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp l₁ l₂)
                                          (CategoryTheory.CategoryStruct.comp k₁ k₂))