{J : Type w} →
  {C : Type uC} →
    {inst : CategoryTheory.Category.{uC', uC} C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {F : J → C} →
          {P : Sort u} →
            {pt : C} →
              {π : (j : J) → pt ⟶ F j} →
                {ι : (j : J) → F j ⟶ pt} →
                  {ι_π :
                      autoParam
                        (∀ (j j' : J),
                          CategoryTheory.CategoryStruct.comp (ι j) (π j') =
                            if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
                        CategoryTheory.Limits.Bicone.ι_π._autoParam} →
                    {pt' : C} →
                      {π' : (j : J) → pt' ⟶ F j} →
                        {ι' : (j : J) → F j ⟶ pt'} →
                          {ι_π' :
                              autoParam
                                (∀ (j j' : J),
                                  CategoryTheory.CategoryStruct.comp (ι' j) (π' j') =
                                    if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
                                CategoryTheory.Limits.Bicone.ι_π._autoParam} →
                            { pt := pt, π := π, ι := ι, ι_π := ι_π } = { pt := pt', π := π', ι := ι', ι_π := ι_π' } →
                              (pt ≍ pt' → π ≍ π' → ι ≍ ι' → P) → P