∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).inl = b.ι CategoryTheory.Limits.WalkingPair.left