where: comp(f,g) is the composition of arrow f followed by and arrow g
Note the order of arguments -- a minor departure from the usual presentation. In a graphical sense, the comp(f,g) operator is similar to the addition of vectors with the head of arrow f being place at the tail of arrow g.
The source and target of the composition of two arrows must be compatible with the the targets and sources of those two arrows.
5. ALL(f):ALL(g):ALL(h):[f @ arrows & g @ arrows & h @ arrows => [target(f)=source(g) & target(g)=source(h) => comp(comp(f,g),h)=comp(f,comp(g,h))]]
Composition of arrows is associative.
6, ALL(a):ALL(b):[a @ nodes & b @ nodes => ALL(f):[f @ arrows(a,b) <=> f @ arrows & source(f)=a & target(f)=b]]
where: arrows(a,b) is the class of arrows with source a and target b
Although this construction is not referred to by other axioms here, traditionally, it is part of the definition of a category. It may be referred to in other definitions and theorems of category theory.