階数付きトポス

定義（[Forssell–Lumsdaine–Swan 2026, 定義2.2]）: $r$-階数付きトポス ($r\in N\cup \{\infty \}$) とは、NNOを持つ正則圏$\mathcal{E}$ であって、階数列${\mathcal{E}}_0\subseteq {\mathcal{E}}_1\subseteq \cdots \subseteq \mathcal{E}$（部分圏で ${\mathcal{E}}_{\infty }={\bigcup }_r{\mathcal{E}}_r$）を持ち、各 ${\mathcal{E}}_i$はNNOを含む正則部分圏であり、各 $0\le i<r-1$ について ${\mathcal{E}}_i$の各対象が $\mathcal{E}$内に ${\mathcal{E}}_{i+1}$ に属する冪対象を持つもの。

直観的には、型の階数（ネストの深さ）を制限したトポス。例えば$r=1$では量化・関数適用の深さが$1$まで。

重要な性質

• 命題2.6: ${\mathcal{F}}_{\infty }\cong {\mathrm{colim}}_{r\in N}{\mathcal{F}}_r$（コンパクト性、[Forssell–Lumsdaine–Swan 2026, 命題2.6]）
• 命題2.14: 自由$\infty$-階数付きトポス $\simeq$自由トポス（[Forssell–Lumsdaine–Swan 2026, 命題2.14]）
• 命題2.16: ${\mathcal{F}}_r$の終対象$1$は射影的（[Forssell–Lumsdaine–Swan 2026, 命題2.16]）

意義

階数付きトポスの導入により、有限階数の近似→ 内部化可能→内部グルーイング、という戦略が可能になる。これが$N$の射影性証明において核心的な役割を果たす。

関連ページ

• free-topos
• projectivity-of-N
• arithmetic-universe

出典

• Forssell, H., Lumsdaine, P. L., & Swan, A. W. (2026). Makkai’s Lost Proof of Projectivity of N in the Free Topos. arXiv:2604.01139v2 [math.LO]. https://arxiv.org/abs/2604.01139