There's a nice result from here that I wanted to share. The result is that the pullback of a monomorphism is a monomorphism.

Technically speaking, with the diagram to the right, the pullback of a corner $A\to C \leftarrowtail B$ is the object $L$ and the pair of maps $P_1, P_2$. Thus, more formally, the result is that $P_1$ (i.e., the pullback of $m$ along $f$) is a monomorphism.

I'm told this result is important to understand some of topos theory—in particular, subobject classifiers—but my understanding of topos theory is currently lacking. Perhaps another day.

In proving the morphism $P_1$ is a monomorphism, we need that $\forall x, y.\ \ x ; P_1 = y ; P_1 \Rightarrow x = y$ (think injective functions in $\text{Set}$).

Proof Strategy. We take the following steps to prove this result:

1. Consider an object $H$ with morphisms $x, y : H \to L$ and suppose that $x ; P_1 = y ; P_1$.
2. Show that $H$ forms two candidates for the pullback square: one using compositions involving $x$ and one using compositions involving $y$.
3. Each candidate shows the existence of a unique morphism $k: H \to L$ that makes a particular diagram commute, but since the morphism is unique, we must have that certain equalities hold between the diagrams induced by each candidate.
4. We conclude from these equalities that $x$ must be equal to $y$, meaning $P_1$ is a monomorphism.

Suppose the following two diagrams

Then we have two potential candidates for our pullback square

but in order to demonstrate the existence of $k : H \to L$, the definition of a pullback insists we produce the following commutative squares:

We'll restrict our attention to the diagram involving $x$, and the same proof will hold for $y$ by renaming. First, note that we have the following from the definition of composition:

Attaching these diagrams to the one above then yields

which contains the proof goal as a subdiagram. Thus, $H$ indeed forms two candidates for the pullback square, and we have the following holds