{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ X₄ : C} →
      (f₁₂ : X₁ ⟶ X₂) →
        (f₁₃ : X₁ ⟶ X₃) →
          (f₂₄ : X₂ ⟶ X₄) →
            (f₃₄ : X₃ ⟶ X₄) →
              CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄ →
                CategoryTheory.Square C