(X Y : CondensedSet) →
  CategoryTheory.Limits.IsLimit
    (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))