∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).obj CategoryTheory.Limits.WalkingReflexivePair.one = A