CatDat

Implication Details

Claim: If a category is countably distributive, then it has a parametrized natural numbers object.

Proof: Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. Define $z \coloneqq i_0 : 1 \to N$ and $s : N \to N$ by $s \circ i_n \coloneqq i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$ and $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$, while the condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. Thus, the morphisms $\phi_n$ are recursively determined; concretely, $\phi_n = g^n \circ f$.