This post will give a short proof of why $\text{Hom}(X, -)$ forms a functor. For those who aren't aware, $\text{Hom}(X, Y)$ denotes the set of morphisms between objects $X$ and $Y$ in a category $\mathbb{C}$.

<aside> 🕰️ $\text{Hom}$ here stands for "homomorphism". Category theory was forged by generalizing the idea of transformations between algebraic structures, so often times the morphisms between objects were homomorphisms. This notation is just a bit of legacy code that's stuck around.

</aside>

The dash in $\text{Hom}(X, -)$ denotes an implicit lambda which accepts objects in $\mathbb{C}$, forming a mapping from objects in $\mathbb{C}$ to objects in $\text{Set}$, since it's the $\text{Hom}$ set.

Now, the title of the post states that $\text{Hom}(X, -)$ forms a functor—not that it is a functor. That's because it only gives us a mapping on objects, and we need to come up with a suitable mapping on morphisms.

For each $g : A \to B$, where $A, B \in \mathbb{C}$, we define $\text{Hom}(X, g)$ to accept morphisms $f : X \to A$, and map them to composite morphisms $f ; g : X \to B$. Succinctly, this is

$$ \text{Hom}(X, g) \coloneqq f \mapsto f ; g $$

We'd like to show that this definition is a functor, but before we do so, let's get our bearings by looking at an example:

https://s3-us-west-2.amazonaws.com/secure.notion-static.com/aba296b5-6536-433a-b0af-7006ac690cfe/IMG_48B7AD37F541-1.jpeg

What's important to note here is that we don't collapse any structure, and the interesting part of $\text{Hom}(X, -)$ is instead what's going on inside each of the objects and morphisms in the image. For example, $\text{Hom}(X, h)$ maps each morphism in $\text{Hom}(X, A)$ to the composite formed by composing with $h$:

https://s3-us-west-2.amazonaws.com/secure.notion-static.com/12a8656a-ed53-4e7e-96d3-a3aa1e76d27f/IMG_0935BD9301BF-1.jpeg

Then, because we always have the trivial composite $1_X ; m$ for any $m : X \to C$, we have the following morphisms out of $\text{Hom}(X, X)$:

https://s3-us-west-2.amazonaws.com/secure.notion-static.com/37ba299b-3fc0-4af2-88d9-f062bcd4b2fe/IMG_498C6AA271F0-1.jpeg

Now, let's prove this definition is a functor.

Proof

Preservation of Identities. To show this mapping preserves identities, we need to show

$$ \text{Hom}(X, 1_A) = 1_{\text{Hom}(X, A)} $$

Expanding definitions, we have

$$ \begin{align*} \text{Hom}(X, 1_A) & = (f : X \to A) \mapsto f ; 1_A \\ & = f \mapsto f \\ & = 1_{\text{Hom}(X, A)} \end{align*} $$

The last line follows from the fact that the line above is the identity function on morphisms of type $X \to A$, meaning it's the identity morphism of the set $\text{Hom}(X, A)$. Thus, this functor preserves identities.

Preservation of Composition. To show this mapping preserves composition, we must show