logicmatters Category Theory, A Gentle Introduction. by Peter Smith
A category C comprises 2 kinds of things:
governed by the following axioms:
For each arrow f, there are unique associated objects src(f) and tar(f),
respectively the source and target of f; not necessarily distinct.
We write `f:A→B' or `Af→B' to notate that f is an arrow with src(f) A and
tar(f) B.
For any two arrows f:A→B, g:B→C, where src(g) = tar(f),
there exists an arrow g∘f:A→C, `g following f', which we call the composite
of f with g.
Given any object A, there is an arrow 1_{A}:A→A called the identity arrow on A.
For any f:A→B, g:B→C, h:C→D, we have h∘(g∘f) = (h∘g)∘f
For any f:A→B we have f∘1_{A} = f = 1_{B}∘f