In contrast to, for example, Lagrange's theorem: it contains the notion of the "order" of a group, which I guess cannot be defined in terms of morphisms and composition.

Perhaps the "order" cannot be defined, but "order divisible by a prime p" can be defined by: there is a non-trivial map from the cyclic group of order p. The Lagrange theorem then leads to a reformulation of the notion of a p-group in terms of weak factorisation systems/Quillen lifting property, see Thm.2.2(6) of (Formulating basic notions of finite group theory via the lifting property) for this and other reformulations of properties of finite groups in similar terms.