>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)](http://mishap.sdf.org//treplo-groups.pdf) for this and other reformulations of properties of finite groups in similar terms.