階数付きトポス
定義(2.2): r-階数付きトポス(r ∈ N∪{∞})とは、NNO を持つ正則圏 ℰ であって、階数列 ℰ_0 ⊆ ℰ_1 ⊆ … ⊆ ℰ (部分圏で ℰ_∞ = ∪_r ℰ_r)を持ち、各 ℰ_i は NNO を含む正則部分圏であり、各 0 ≤ i < r−1 について ℰ_i の各対象が ℰ 内に ℰ_{i+1} に属する冪対象を持つもの。
直観的には、型の階数(ネストの深さ)を制限したトポス。例えば r=1 では量化・関数適用の深さが 1 まで。
重要な性質
- 命題 2.6: ℱ_∞ ≅ colim_{r∈N} ℱ_r(コンパクト性)
- 命題 2.14: 自由 ∞-階数付きトポス ≃ 自由トポス
- 命題 2.16: ℱ_r の終対象 1 は射影的
意義
階数付きトポスの導入により、有限階数の近似 → 内部化可能 → 内部グルーイング、という戦略が可能になる。これが N の射影性証明において核心的な役割を果たす。