∀ {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) (j : P.I),
  CategoryTheory.CategoryStruct.comp ({ pt := A, ι := P.ι₁ }.ι.app j)
      (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 ({ pt := A, ι := P.ι₁ }.ι.app j)
      (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))