{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (P : CategoryTheory.IndParallelPairPresentation f g) →
          CategoryTheory.Limits.parallelPair f g ≅
            (CategoryTheory.Limits.parallelPair P.φ P.ψ).comp
              (((CategoryTheory.Functor.whiskeringRight P.I C (CategoryTheory.Functor Cᵒᵖ (Type v₁))).obj
                    CategoryTheory.yoneda).comp
                CategoryTheory.Limits.colim)