In Eugenia Cheng's The Joy of Abstraction, the author discusses a categorical definition of the notion of category. This definition turns out to be useful to define the notion of internal category. The author gives part of the definition and challenges the reader to formulate the rest. I came up with an answer but I'm not sure if it's right.
Background: A category requires an object of objects $C_0$ and an object of morphisms $C_1$, with source and target morphisms: $$s, t : C_1 \rightarrow C_0$$ Intuitively, if $f : a \rightarrow b$ is a morphism in $C_1$, $s(f)$ is the source of the morphism, i.e. $a$, and $t(f)$ is the target, i.e. $b$.
There is a morphism $$id : C_0 \rightarrow C_1$$ which (intuitively) returns for each object $a$ in $C_0$ the identity morphism $1_a$.
Finally, there is a morphism $$cp : (C_1 \times_{C_0} C_1) \rightarrow C_1 $$ which encapsulates the composition of morphisms in $C_1$. The object $C_1 \times_{C_0} C_1$ is a pullback formed from $s$ and $t$, which represents composable pairs of morphisms.
The challenge: formulate the unit law $f \circ 1_a = f$ categorically. (The other unit law can have an analogous formulation.)
My solution: First, we need to form a pullback:
$$\require{AMScd} \begin{CD} (C_1 \times_{C_1} C_1) @>{p_2}>> C_1 \\ @V{p_1}VV @VV{id \circ s}V \\ C_1 @>>{1_{C_1}}> C_1 \end{CD} $$
Thinking about this in the context of the category Set, $(C_1 \times_{C_1} C_1)$ is the set of pairs $(g, f)$ where $1_{C_1}(g) = g = id(s(f))$. In other words, $g$ is the identity on whatever $f$'s source is: $1_{s(f)}$. Such a pair $(1_{s(f)}, f)$ is always composable (the composition is $f \circ 1_{s(f)}$). Therefore there should be an inclusion between the pullbacks $j : (C_1 \times_{C_1} C_1) \rightarrow (C_1 \times_{C_0} C_1)$. However, I don't know how to define this precisely.
We should be able to express one of the unit laws by saying that, in the following diagram, $p_2 = (cp)j$: $$\require{AMScd} \begin{CD} (C_1 \times_{C_1} C_1) @>{j}>> (C_1 \times_{C_0} C_1) @>{cp}>> C_1 \\ @V{p_2}VV \\ C_1 \end{CD}$$
Thinking in Set again: given a pair $(1_{s(f)}, f)$, the composition $f \circ 1_{s(f)}$ is identical to the second co-ordinate of the pair, $f$.
There is a map $(1_{C_1},\mathrm{id}\circ s)\colon C_1\to C_1\times_{C_0}C_1$ by the universal property of the pullback, since $s\circ 1_{C_1} = s = t\circ \mathrm{id}\circ s$. Intuitively, this map sends an arrow $f\colon a\to b$ to the composable pair $(f,\mathrm{id}_a)$. Now the unit law just says $\mathrm{cp}\circ (1_{C_1},\mathrm{id}\circ s)=1_{C_1}$, which can be expressed by the commutativity of a triangular diagram.