Does the morphism of composition have some universal property?

Question

Let $A$, $B$ and $C$ be three objects in the category Set. For simplicity, assume that their underlying sets contain a finite number of elements, a, b and c respectively. Using the usual Haskell notation for types, there exists exactly $(c^a)^{c^b×b^a}$ morphisms from the object/type ($b\rightarrow c$, $a\rightarrow b$) to the object/type $a\rightarrow c$. Among this potentially huge set of morphisms, exactly one is the (uncurried) composition function, defined as ${\rm compose}\, (g, f) = g\circ f$.

My question is, does this particular morphism have any universal property that make it possible to identify using only category theory?

This is the computer-scientist-toying-with-categories-version of the question. If you prefer a version written by a proper mathematician, please refer to The universal property of composition of morphisms

Answer 1

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$

2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

   $$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.