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

TL;DR

This paper provides a categorical proof of the projectivity of N in the free topos, based on Makkai's unpublished proof, connecting to countable choice in higher-order logic.

Contribution

It offers a new, self-contained categorical proof of N's projectivity, revisiting Makkai's lost proof and clarifying its proof-theoretic implications.

Findings

Confirmed the projectivity of N in the free topos

Connected the proof to countable choice in higher-order logic

Presented an accessible, self-contained proof

Abstract

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 the unpublished proof of Michael Makkai (c.1980). The presentation aims to be self-contained and accessible to any reader acquainted with elementary toposes and their logic.