∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ e₀_1 :
    F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e_e₀ : e₀ = e₀_1)
  (e₁ e₁_1 :
    F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (e_e₁ : e₁ = e₁_1)
  (h₁ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
  (h₂ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
      CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
  (h₃ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
      CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)),
  CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ h₁ h₂ h₃ =
    CategoryTheory.Limits.reflexivePair.mkNatTrans e₀_1 e₁_1 ⋯ ⋯ ⋯