Cancellation of products in an arbitrary category does not hold; does it hold with this extra condition? Let $\mathcal{C}$ be a category with products, and let $A,B,C$ be objects of $\mathcal{C}$. Certainly, it need not be true that
$$A\times B\cong A\times C\implies B\cong C.$$
For an easy example, we could have $\mathcal{C}=\mathsf{Set}$, with $A$ an infinite set, and with $B$ and $C$ finite sets of different cardinalities. There are perhaps more surprising examples with topological spaces (see this MathOverflow thread).
Let $p\colon A\times B\to A$ and $q\colon A\times C\to A$ be these products' respective projection maps to $A$. Suppose there is an isomorphism $f\colon A\times B\to A\times C$ such that $p=q\circ f$. Does this imply $B\cong C$?
I believe the answer is yes - at the very least, this condition rules out the example with sets I mentioned above - but a proof (or counterexample) is eluding me at the moment. Any help would be appreciated.
 A: Assume that $A$ has some global element, i.e. a morphism $* \to A$ where $*$ is a terminal object. Then an isomorphism $A \times B \cong A \times C$ over $A$ induces an isomorphism $* \times_A (A \times B) \cong * \times_A (A \times C)$ over $*$. But $* \times_A (A \times B) \cong * \times B \cong B$ and likewise $* \times_A (A \times C) \cong C$.
A: Your claim is false for silly reasons: take $A = \emptyset$ in $\mathbf{Set}$, for example. It is also false for more subtle reasons: take $X$ to be a space, $C$ a non-trivial vector bundle on $X$ of rank $r$, $B$ a trivial vector bundle on $X$ of rank $r$, and $A$ the disjoint union of a trivialising open cover for $C$, all this in $\mathbf{Top}_{/ X}$.
But here is a more positive result:
Proposition. If $\mathcal{C}$ is a regular category and $x : I \to J$ is a regular epimorphism in $\mathcal{C}$, then the pullback functor $x^* : \mathcal{C}_{/ J} \to \mathcal{C}_{/ I}$ (i.e. the functor $A \mapsto I \times_J A$) is conservative.
Proof. Let $k_0, k_1 : K \to I$ be the kernel pair of $x : I \to J$. Since $x$ is a regular epimorphism, $x$ is the coequaliser of $k_0$ and $k_1$. Let $f : A \to B$ be a morphism in $\mathcal{C}_{/ J}$. Then we can form a commutative diagram in $\mathcal{C}$ as below,
$$\begin{array}{ccccc}
K \times_J A & \rightrightarrows & I \times_J A & \rightarrow & A \\
\downarrow & & \downarrow & & \downarrow \\
K \times_J B & \rightrightarrows & I \times_J B & \rightarrow & B
\end{array}$$
where the rows are exact, meaning the left half is the kernel pair of the right half and the right half is the coequaliser of the left half. It is clear that $f : A \to B$ is the unique morphism $A \to B$ that makes the diagram commute. Thus, $f : A \to B$ is an isomorphism if and only if $x^* f : I \times_J A \to I \times_J B$ is an isomorphism. 　◼
The question of when the existence of an isomorphism in $\mathcal{C}_{/ I}$ implies the existence of an isomorphism in $\mathcal{C}_{/ J}$ is more subtle. For this what we need is an effective regular category: then we can apply descent theory to manufacture an isomorphism in $\mathcal{C}_{/ J}$ from an isomorphism in $\mathcal{C}_{/ I}$ satisfying some conditions.
