nlab suggests falling back to pullbacks to internalize the single sorted definition of a category. But can we internalize single sorted categories here without pullbacks?
I have an idea but I'm not quite sure it makes sense. I have a hunch it's sort of equivalent to proving pullbacks exist anyway? It's sort of like "Closed Cartesian" where you don't actually have a Cartesian product but the concept is basically equivalent to having one. I think this is sort of like using Cartesian products anyhow even if they aren't explicitly mentioned.
Source
$$ \text{s}\colon \text{Hom}(C, C) $$
Target
$$ \text{t}\colon \text{Hom}(C, C) $$
Composition
$$ - \cdot -\colon \forall A, \{ f\colon \text{Hom}(A, C), g \colon \text{Hom}(A, C) \mid \text{s} \circ f = \text{t} \circ g \} \rightarrow \text{Hom}(A , C )$$
Identity
$$ (\text{t} \circ f) \cdot f = f$$ $$ f \cdot (\text{s} \circ f) = f$$
Associativity
$$(f \cdot g) \cdot h = f \cdot (g \cdot h)$$
Then the usual rules for the source and target of an object.
$$ \text{s} \circ \text{s} = \text{t} \circ \text{s} = \text{s} $$
$$ \text{s} \circ \text{t} = \text{t} \circ \text{t} = \text{t}$$
I have a feeling you also want some kind of naturality rule something like
$$ (f \circ h) \cdot (g \circ h) = (f \cdot g) \circ h $$