{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {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) →
                  (F : CategoryTheory.Functor C D) →
                    (CategoryTheory.Limits.reflexivePair f g s sl sr).comp F ≅
                      CategoryTheory.Limits.reflexivePair (F.map f) (F.map g) (F.map s) ⋯ ⋯