∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} {X : Type u₇} {Y : Type u₈}
  {Z : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] [inst_3 : CategoryTheory.Category.{v₄, u₄} D]
  [inst_4 : CategoryTheory.Category.{v₅, u₅} E] [inst_5 : CategoryTheory.Category.{v₆, u₆} F]
  [inst_6 : CategoryTheory.Category.{v₇, u₇} X] [inst_7 : CategoryTheory.Category.{v₈, u₈} Y]
  [inst_8 : CategoryTheory.Category.{v₉, u₉} Z] {G₁ : CategoryTheory.Functor A D} {H₁ : CategoryTheory.Functor B E}
  {K₁ : CategoryTheory.Functor C F} {G₂ : CategoryTheory.Functor D X} {H₂ : CategoryTheory.Functor E Y}
  {K₂ : CategoryTheory.Functor F Z} {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A}
  {L₂ : CategoryTheory.Functor B C} {R₂ : CategoryTheory.Functor C B} {L₃ : CategoryTheory.Functor D E}
  {R₃ : CategoryTheory.Functor E D} {L₄ : CategoryTheory.Functor E F} {R₄ : CategoryTheory.Functor F E}
  {L₅ : CategoryTheory.Functor X Y} {R₅ : CategoryTheory.Functor Y X} {L₆ : CategoryTheory.Functor Y Z}
  {R₆ : CategoryTheory.Functor Z Y} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (adj₄ : L₄ ⊣ R₄) (adj₅ : L₅ ⊣ R₅)
  (adj₆ : L₆ ⊣ R₆) (α : CategoryTheory.TwoSquare G₁ L₁ L₃ H₁) (β : CategoryTheory.TwoSquare H₁ L₂ L₄ K₁)
  (γ : CategoryTheory.TwoSquare G₂ L₃ L₅ H₂) (δ : CategoryTheory.TwoSquare H₂ L₄ L₆ K₂),
  (CategoryTheory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α.vComp β).hComp (γ.vComp δ)) =
    (((CategoryTheory.mateEquiv adj₂ adj₄) β).hComp ((CategoryTheory.mateEquiv adj₁ adj₃) α)).vComp
      (((CategoryTheory.mateEquiv adj₄ adj₆) δ).hComp ((CategoryTheory.mateEquiv adj₃ adj₅) γ))