definition. binary product [kostecki2011introduction, 2.18] [tt-000Y]
A binary product of objects \(X\) and \(Y\) is an object \(X \times Y\) in \({\cal C}\) together with arrows \(p_X\) and \(p_Y\), called projections, such that, for any object \(\mathrm {-}\) and arrows \(h\) and \(k\), the diagram
definition. binary product [kostecki2011introduction, 2.18] [tt-000Y]
commutes.
We say that a category \({\cal C}\) has binary products iff every pair \(X, Y\) in \({\cal C}\) has a binary product \(X \times Y\) in \({\cal C}\).
When there is no confusion, we simply call bianry products products.