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