Todd Trimble distributivity implies monicity of coproduct inclusions

Proof

Let $i_B: B \to B + C$ be a coproduct inclusion, and suppose given maps $f, g: A \to B$ such that $i_B f = i_B g$. We observe that the coproduct inclusion

is monic because it has a retraction $(1_{A \times B}, \phi): A \times B + A \times C \to A \times B$. (All we need here is the existence of a map $\phi: A \times C \to A \times B$, for example the composite $A \times C \stackrel{\pi_A}{\to} A \stackrel{\langle 1_A, f \rangle}{\to} A \times B$.)

The composite of the coproduct inclusion $i$ with the canonical isomorphism $A \times B + A \times C \cong A \times (B + C)$, namely $1_A \times i_B: A \times B \to A \times (B + C)$, is therefore also monic. Given that $\langle 1_A, i_B f \rangle = \langle 1_A, i_B g \rangle: A \to A \times (B + C)$, we conclude

whence $\langle 1_A, f\rangle = \langle 1_A, g\rangle$ since $1_A \times i_B$ is monic. It follows that $f = g$, as was to be shown.

Proof

Clearly for any $Y$ the hom-set $\hom(X \times 0, Y)$ is inhabited by $X \times 0 \to 0 \to Y$, and so we only need show that any two $f, g: X \times 0 \to Y$ are equal. By the proposition above, it suffices that any two $f, g: X \times 0 \to X + Y$ are equal.

The coproduct inclusion $X \hookrightarrow X \times 0 + X$ is an isomorphism $X \cong X \times 1 \cong X \times (0 + 1) \cong X \times 0 + X \times 1 \cong X \times 0 + X$, so that the projection

is an isomorphism of sets for any object $A$. As soon as $\hom(X, A)$ is inhabited, this means $\hom(X \times 0, A)$ must be a singleton. In particular, $\hom(X \times 0, X + Y)$ is a singleton, which is just what we wanted.