∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} [inst_2 : SizeOf C] (hom : A.pt ⟶ B.pt)
  (wfst :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam)
  (wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam)
  (winl :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam)
  (winr :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam),
  sizeOf { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
    1 + sizeOf hom + sizeOf wfst + sizeOf wsnd + sizeOf winl + sizeOf winr