There are many axiom systems for natural numbers. My favorites are 1. Heyting Arithmetic, and 2. In category theory, one can characterise the natural numbers and the initial algebra of the X |–> X+1. functor.
Category Theory itself assumes the existence of natural numbers. My point was about whether their futher "axiomatization" via a functor makes it easier to prove theorems or make discoveries.
