∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type u_2)}
  {f g : A ⟶ B} (P : CategoryTheory.IndParallelPairPresentation f g),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.parallelPair f g).map CategoryTheory.Limits.WalkingParallelPairHom.right)
      (P.isColimit₂.coconePointUniqueUpToIso
          (CategoryTheory.Limits.colimit.isColimit (P.F₂.comp CategoryTheory.yoneda))).hom =
    CategoryTheory.CategoryStruct.comp
      (P.isColimit₁.coconePointUniqueUpToIso
          (CategoryTheory.Limits.colimit.isColimit (P.F₁.comp CategoryTheory.yoneda))).hom
      (((CategoryTheory.Limits.parallelPair P.φ P.ψ).comp
            (((CategoryTheory.Functor.whiskeringRight P.I C (CategoryTheory.Functor Cᵒᵖ (Type u_2))).obj
                  CategoryTheory.yoneda).comp
              CategoryTheory.Limits.colim)).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)