Makkai's lost proof of projectivity of N in the free topos
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914525729521664 |
|---|---|
| author | Forssell, Henrik Lumsdaine, Peter LeFanu Swan, Andrew W. |
| author_facet | Forssell, Henrik Lumsdaine, Peter LeFanu Swan, Andrew W. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_01139 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Makkai's lost proof of projectivity of N in the free topos Forssell, Henrik Lumsdaine, Peter LeFanu Swan, Andrew W. Logic Category Theory 03G30 Categorical logic, topoi (primary), 03F50 Metamathematics of constructive systems, 03B16 Higher-order logic 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. |
| title | Makkai's lost proof of projectivity of N in the free topos |
| topic | Logic Category Theory 03G30 Categorical logic, topoi (primary), 03F50 Metamathematics of constructive systems, 03B16 Higher-order logic |
| url | https://arxiv.org/abs/2604.01139 |