∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : 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] {G : CategoryTheory.Functor A C} {H : CategoryTheory.Functor B D}
  {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor C D}
  {R₂ : CategoryTheory.Functor D C} {L₃ : CategoryTheory.Functor C D} {R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : CategoryTheory.TwoSquare G L₁ L₂ H) (β : L₃ ⟶ L₂),
  (CategoryTheory.mateEquiv adj₁ adj₃) (α.whiskerRight β) =
    ((CategoryTheory.mateEquiv adj₁ adj₂) α).whiskerBottom ((CategoryTheory.conjugateEquiv adj₂ adj₃) β)