IV.P148 — NNO from the alpha-Orbit

The alpha-orbit O_alpha = {alpha_n : n >= 1} with initial element alpha_1 = alpha and successor map rho|_{O_alpha} is a Natural Number Object (NNO) in the categorical sense: for any object C with c_0 and endomorphism s, there exists a unique f : O_alpha -> C with f(alpha_1) = c_0 and f o rho = s o f.