Dinatural numbers Original Research Article

The notion of strong Barr dinatural transformation is introduced which, when taken between Hom functors, gives a notion of natural number specifically adapted to the category under consideration. We call these dinatural numbers and we study their arithmetic which depends in a nice way on the structure of the category. We also consider families of dinatural numbers, which leads to a new universal property for natural numbers object as classifying object for dinatural numbers. When there is a natural numbers object, its arithmetic defined by recursion corresponds to the arithmetic of dinatural numbers. Examples are given with a particular emphasis on the category of finite sets.