{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
        {f g : A ⟶ B} →
          {t : CategoryTheory.IndParallelPairPresentation f g} →
            {C' : Type u₁} →
              {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                {A' B' : CategoryTheory.Functor C'ᵒᵖ (Type v₁)} →
                  {f' g' : A' ⟶ B'} →
                    {t' : CategoryTheory.IndParallelPairPresentation f' g'} →
                      C = C' →
                        inst ≍ inst' →
                          A ≍ A' →
                            B ≍ B' →
                              f ≍ f' →
                                g ≍ g' → t ≍ t' → CategoryTheory.IndParallelPairPresentation.noConfusionType P t t'