I've just started working on proofs in category theory and I'm interested in thinking about the structure of a proof in terms of this domain. This means thinking about the proof in terms of arrows rather than objects in Set (or functions applied to objects). For those who are interested, I'm working through Goldblatt's Topoi: The Categorial Analysis of Logic.
One of the early exercises in the book is to prove that $f\circ g$ is monic if $f$ and $g$ are monic. A proof I worked out follows. Any and all comments on the structure or conventions of proof in category theory would be much appreciated. Thanks.
Proof:
Assume $f: A\rightarrowtail B$ and $g: B\rightarrowtail C$ in some category C
By definition of monic:
$\forall$ C-arrows $h,i: D\rightrightarrows A$, $f\circ h = f\circ i$ and $h = i$ (left-cancellation)
Similarly,
$g\circ (f\circ h) = g\circ (f\circ i)$
And, by associativity of composition,
$(g\circ f)\circ h = (g\circ f)\circ i$
which with the known $h = i$ (edit: via $f$'s monicity) demonstrates left-cancellation of $g\circ f$ and the definition of monic. $\Box$
You have to apply the definition twice. We want to show that $(g \circ f) \circ h = (g \circ f) \circ i$ implies $h = i$. As you mention, composition is associative, so the hypothesis is equivalent to $g \circ (f \circ h) = g \circ (f \circ i)$. Since $g$ is monic, we must have $f \circ h = f \circ i$. But since $f$ is monic, this implies that $h = i$ as desired.