{P : Sort u} →
  {C : Type u_1} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {S₁ S₂ : CategoryTheory.ShortComplex C} →
          {t : S₁.Hom S₂} →
            {C' : Type u_1} →
              {inst' : CategoryTheory.Category.{v_1, u_1} C'} →
                {inst'_1 : CategoryTheory.Limits.HasZeroMorphisms C'} →
                  {S₁' S₂' : CategoryTheory.ShortComplex C'} →
                    {t' : S₁'.Hom S₂'} →
                      C = C' →
                        inst ≍ inst' →
                          inst_1 ≍ inst'_1 →
                            S₁ ≍ S₁' → S₂ ≍ S₂' → t ≍ t' → CategoryTheory.ShortComplex.Hom.noConfusionType P t t'