{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X Y : C) →
      (p : {Z : C} → (X ⟶ Z) → (Y ⟶ Z)) →
        (q : {Z : C} → (Y ⟶ Z) → (X ⟶ Z)) →
          (∀ {Z : C} (f : X ⟶ Z), q (p f) = f) →
            (∀ {Z : C} (f : Y ⟶ Z), p (q f) = f) →
              (∀ {Z Z' : C} (f : Y ⟶ Z) (g : Z ⟶ Z'),
                  q (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (q f) g) →
                (X ≅ Y)