Let $I$ be the subset $[0,1]\subset \mathbb R$. For any set $S$, let $i_S:S\to I\times S$ be the map defined by $i_S(s)=(0,s)$ for all $s\in S$.$ \require{AMScd}$
Let $i:A\to X$ be a map of sets, and consider the following square.
$$\begin{CD} A@>i_A>> I\times A\\ @VViV @VV\mathrm{id}_I\times iV \\ X@>{i_X}>> I\times X \end{CD}$$
Letting $P:= X\sqcup _A(I\times A)$, and $p_X$, $p_{I\times A}$ be the canonical maps into $P$, the universal property of pushouts yields a map $j:P\to I\times X$, such that $j\circ p_X=i_X$ and $j\circ p_{I\times A}=\mathrm{id}_I\times i$.
Now suppose that there is a map $r:I\times X\to P$ satisfying $r\circ i_X=p_X $ and $r\circ (\mathrm{id}_I\times i)=p_{I\times A}$. In this case follows that $r\circ j=\mathrm{id}_P$.
Question. Is $i$ injective?
Injective maps in our picture surely are $j$, $i_A$, $i_X$ and $p_X$. In order to show that $i$ is injective, I tried to prove that either $p_{I\times A}$ or (eqivalently) $\mathrm {id}_I\times i$ is injective, and I also tried to induce some map $P\to A$ or $P\to I\times A$, but without any result.
I've been stuck for a while on this task, although it seems easy; would you just give me a suggestion? Thanks in advance
Since we are working in the category of sets, we will use the internal description of the pushout $P$ and the map $j$.
$P = X \coprod (I\times A)/\sim$ where $\sim$ is the equivalence closure of the relation identifying $i(a)$ with $(0,a)$ for each $a \in A$. The maps in the pushout square are the obvious "embeddings".
The map $j : P \to I \times X$ sends $[x] \mapsto (0,x)$ and $[(t,a)] \mapsto (t,i(a))$.
Now, observe that since $r$ is a retraction (left inverse) of $j$, hence $j$ is injective.
Suppose that $i(a) = i(b)$ for some $a,b \in A$. Then, $j([(1,a)]) = (1,i(a)) = (1,i(b)) = j([(1,b)])$ so that, $[(1,a)] = [(1,b)]$ and hence, $(1,a) \sim (1,b)$. But the equivalence class of any element $(t,p) \in I \times A$, where $t > 0$, is a singleton. Hence, $(1,a) \sim (1,b)$ implies that $a = b$. Hence, $i$ is injective.
Note : The presence of an element other than $0$ in $I$ actually guarantees the injectivity of $I$
The last remark actually is helpful, in that the above statement is valid in categories with a special property.
Let $\mathcal{C}$ be a category with the following properties :
It has pushouts and finite products (in particular, a terminal object $1$).
There is an object $I$ with two distinct arrows $a,b : 1 \rightarrow I$ (such an arrow is called a generalized element of $I$, in that, it detects "elements" in $I$ (even though, $I$, being an object in an abstract category, has no notion of elements belonging to it).
Then, your problem can be formulated as follows :
For any object $S$ in $\mathcal{C}$, let $S \xrightarrow{i_S} I \times S$ be the unique arrow induced by $(S \to 1 \xrightarrow{a} I, S \xrightarrow{1_S})$. The first component of this pair actually denotes a "constant map" from $S$ to $I$. Note that $i_S$ is a section of the projection $I \times S \to S$, so that $i_S$ is a monomorphism.
Now, let $i : A \to X$ be an arrow in $\mathcal{C}$.
Note that the diagram
$\require{AMScd}$ \begin{CD} A @>{i_A}>> I \times A\\ @V{i}VV @V{1_I \times i}VV\\ X @>{i_X}>> I \times X \end{CD} is commutative.
Form the pushout $P = X \coprod_{A} (I \times A)$ and let the unique map $j : P \to I \times X$ be a split monomorphism (this is equivalent to the existence of a morphism $r : I \times X \to P$ satisfying the two equations as mentioned in your question).
Then, $i$ is a monomorphism.
The proof of this will use the same idea, that is, the existence of the generalized element $b : 1 \to I$, which is different from $a : 1\to I$.