{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {X Y : C} →
      {P : Sort u_1} →
        {i : X ⟶ Y} →
          {r : Y ⟶ X} →
            {retract :
                autoParam (CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X)
                  CategoryTheory.Retract.retract._autoParam} →
              {i' : X ⟶ Y} →
                {r' : Y ⟶ X} →
                  {retract' :
                      autoParam (CategoryTheory.CategoryStruct.comp i' r' = CategoryTheory.CategoryStruct.id X)
                        CategoryTheory.Retract.retract._autoParam} →
                    { i := i, r := r, retract := retract } = { i := i', r := r', retract := retract' } →
                      (i ≍ i' → r ≍ r' → P) → P