{c}
{title2=$\mathsf{Pair}=\lambda a b p.pab$}

With the <Church Booleans> $\mathsf T=\lambda a b.a$ and $\mathsf F=\lambda a b.b$, encode a pair by
$$
\mathsf{Pair}=\lambda a b p.pab,\qquad \mathsf{Fst}=\lambda p.p\mathsf T,\qquad \mathsf{Snd}=\lambda p.p\mathsf F.
$$
Then $\mathsf{Fst}(\mathsf{Pair}\,A\,B)\to_\beta^*A$ and the second projection similarly returns $B$. Pairing an iteration counter with a computed value implements <primitive recursion> using only <Church numeral> iteration.


 Church pair

ID: church-pair