Under which additional conditions $a\times b = c\times d \Rightarrow a=c\wedge b=d$ (where $\times$ is a categorical product)?
For example, in the case of Cartesian product, for this is enough when the factors are non-empty. Can this be generalized?
I'm also interested about the similar construction with infinite product.
On
The question as stated is a little bit ambiguous, but it's not Porton's fault. The truth is the expression $a\times b$ may be interpreted either as a product object (which is defined only up to isomorphism) or as the result of a product bifunctor applied to objects $a$ and $b$, defined on a category with binary products. Ponton's question only makes sense if we consider the second interpretation.
In this sense the OP's question is roughly: under what circumstances/limitations is a product bifunctor injective on objects?
Crucial point to note: if you are given a category with binary products, you can define many products bifunctors. Any two of these bifunctors, $\times'$ and $\times''$, are related by natural isomorphisms.
Suppose you can state the following result for product $\times'$: $\forall(a,b,c,d): P(a,b,c,d)\implies ((a\times' b=c\times'd)\implies (a=c\wedge b=d))$
Where $P(a,b,c,d)$ means that $a,b,c,d$ satisfy predicate $P$ (eg. in $\mathcal{Set}$, $P(a,b,c,d)$ might be "a,b,c,d not empty" )
Can you conclude that the same statement holds for another product $\times''$? $\forall(a,b): P(a,b)\implies ((a\times'' b=c\times''d)\implies (a=c\wedge b=d))$
In general no (although I cannot present a concrete example). So whatever conclusion you may arrive at, it would depend not only on your particular category, but also on the particular product bifunctor you have decided to use in that particular category. This is not likely to be very useful/meaningful.
Apparently, for you $a \times b$ is the set of ordered pairs $\{(x,y) : x \in a, y \in b\}$. Now if $a \times b \subseteq c \times d$ and $b$ is non-empty, then indeed one finds $a \subseteq c$ using the definitions. Similarly, if $d$ is non-empty, the other inclusion will also give the other inclusion $c \subseteq a$. So equality as sets means $a=c$.
Now assume $a \times b$ is understood as the categorical product, i.e. it just some set equipped with projections $p_a : a \times b \to a$ and $p_b : a \times b \to b$ satisfying the universal property. In particular, $a \times b$ is also a version of $b \times a$ (with the projections swapped), and we cannot hope for any cancellation. On the other hand, equality of objects of a category is not an interesting notion; instead the notion of equivalence (see nlab) is more natural and important. But first we have to agree which objects we are talking about. Just the underlying objects $a \times b$ , $c \times d$ yields very boring counterexamples, for example $\{1\} \times \{1,2,3,4\}$ is isomorphic to $\{1,2\} \times \{1,2\}$. Instead, we should also include our projections and take into account the whole product diagram. Then, an isomorphism $(a \times b,p_a,p_b) \to (c \times d,p_c,p_d)$ should be an isomorphism of diagrams $(p_a,p_b) \to (p_c,p_d)$ which induces an isomorphism on the limit (but this is automatic), i.e. just a pair of isomorphisms $a \to c$ and $b \to d$. In this sense we have cancellation, but it is a very trivial result.
Remark that cancellation for underlying objects of products is a quite hard problem in general. For example, in affine algebraic geometry, $X \times \mathbb{A}^1 \cong \mathbb{A}^2 \Rightarrow X \cong \mathbb{A}^1$ and $X \times \mathbb{A}^1 \cong \mathbb{A}^3 \Rightarrow X \cong \mathbb{A}^2$ are well-known, but the corresponding problem in higher dimensions is widely open.