{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (pt : C) →
          (fst : pt ⟶ P) →
            (snd : pt ⟶ Q) →
              (inl : P ⟶ pt) →
                (inr : Q ⟶ pt) →
                  autoParam (CategoryTheory.CategoryStruct.comp inl fst = CategoryTheory.CategoryStruct.id P)
                      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam →
                    autoParam (CategoryTheory.CategoryStruct.comp inl snd = 0)
                        CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam →
                      autoParam (CategoryTheory.CategoryStruct.comp inr fst = 0)
                          CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam →
                        autoParam (CategoryTheory.CategoryStruct.comp inr snd = CategoryTheory.CategoryStruct.id Q)
                            CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam →
                          CategoryTheory.Limits.BinaryBicone P Q