{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {X Y : C} →
      {f : X ⟶ Y} →
        {P : Sort u_1} →
          {I : C} →
            {m : I ⟶ Y} →
              {m_mono : CategoryTheory.Mono m} →
                {e : X ⟶ I} →
                  {fac :
                      autoParam (CategoryTheory.CategoryStruct.comp e m = f)
                        CategoryTheory.Limits.MonoFactorisation.fac._autoParam} →
                    {I' : C} →
                      {m' : I' ⟶ Y} →
                        {m_mono' : CategoryTheory.Mono m'} →
                          {e' : X ⟶ I'} →
                            {fac' :
                                autoParam (CategoryTheory.CategoryStruct.comp e' m' = f)
                                  CategoryTheory.Limits.MonoFactorisation.fac._autoParam} →
                              { I := I, m := m, m_mono := m_mono, e := e, fac := fac } =
                                  { I := I', m := m', m_mono := m_mono', e := e', fac := fac' } →
                                (I ≍ I' → m ≍ m' → e ≍ e' → P) → P