The following image is of an app I'm working on called "Abstract Spacecraft". It will allow you to make logical rules and also apply them to diagrams at the click of a button, should the diagram match the domain of the rule arrow (Axiom, Definition, Notation, Theorem).
I refer to the rule arrow labeled "Notation. arrows compose".
My question is, how do current type systems classify the rule that if you see a composition written $A \xrightarrow{gf} C$, the you can decompose that into two arrows $A \xrightarrow{f} B \xrightarrow{g} C$?
This is just an obvious fact, but in a formal system it can be encoded into a rule. So I'm wondering, is the rule axiomatic, definitional, or notational?
In category theory, you cannot decompose arrows unless you have additional structure like a factorisation system. What you are describing is really a meta-theorem about syntax: if you have an arrow $g \circ f : A \to C$, then you necessarily must have had arrows $f \colon A \to B$ and $g \colon B \to C$ for the notation $g \circ f$ to be well-formed. To make this formal, you would need to be able to describe ill-formed terms as well as well-formed terms, after which you would be able to state a theorem along the lines of: "If the expression $g \circ f$ is well-formed, then so are $g$ and $f$.", which you'd prove by induction over the rules of the syntax. However, in practice, such a result isn't useful: if you're ever in a situation where you're handed a composite $g \circ f$ and wish to decompose it, you could just have been handed the pair $(f, g)$ instead. In other words, you should think of "composable pairs" rather than "composed pairs".