{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone X Y)
          (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))