{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {X Y : C} →
        {f : X ⟶ Y} →
          {t : CategoryTheory.Limits.StrongEpiMonoFactorisation f} →
            {C' : Type u} →
              {inst' : CategoryTheory.Category.{v, u} C'} →
                {X' Y' : C'} →
                  {f' : X' ⟶ Y'} →
                    {t' : CategoryTheory.Limits.StrongEpiMonoFactorisation f'} →
                      C = C' →
                        inst ≍ inst' →
                          X ≍ X' →
                            Y ≍ Y' →
                              f ≍ f' → t ≍ t' → CategoryTheory.Limits.StrongEpiMonoFactorisation.noConfusionType P t t'