CatDat

Implication Details

Claim: If a category is cartesian closed and has a natural numbers object, then it has a parametrized natural numbers object.

Proof: Let $(N,z,s)$ be a natural numbers object in a cartesian closed category. Let $f : A \to X$ and $g : X \to X$ be morphisms. These induce morphisms $\hat{f} : 1 \to [A,X]$ and $g_* : [A,X] \to [A,X]$. By the universal property of $(N,z,s)$, there is a unique morphism $\Psi : N \to [A,X]$ satisfying $\Psi(z) = \hat{f}$ and $\Psi(s(n)) = g_*(\Psi(n))$. By the exponential adjunction, this corresponds to a morphism $\Phi : A \times N \to X$ satisfying $\Phi(a,z) = f(a)$ and $\Phi(a,s(n)) = g(\Phi(a,n))$.