{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {J : Type u_1} →
      {I : J → Type u_2} →
        {inst_1 : CategoryTheory.Category.{v_1, u_1} J} →
          {inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)} →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                {k l : CategoryTheory.Limits.ColimitPresentation.Total P} →
                  {P_1 : Sort u_4} →
                    {base : k.fst ⟶ l.fst} →
                      {hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd} →
                        {w :
                            autoParam
                              (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
                                CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
                              CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam} →
                          {base' : k.fst ⟶ l.fst} →
                            {hom' : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd} →
                              {w' :
                                  autoParam
                                    (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base') =
                                      CategoryTheory.CategoryStruct.comp hom' ((P l.fst).ι.app l.snd))
                                    CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam} →
                                { base := base, hom := hom, w := w } = { base := base', hom := hom', w := w' } →
                                  (base ≍ base' → hom ≍ hom' → P_1) → P_1