Makkai's lost proof of projectivity of N in the free topos

Henrik Forssell, Peter LeFanu Lumsdaine, Andrew W. Swan

We give a categorical proof of the projectivity of $N$ in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on…