自由トポス

自由トポス $\mathcal{F}$とは、トポスの2-圏におけるbi-初始対象。つまり、任意のトポス$\mathcal{E}$に対して一意な（同型を除いた）論理関手 $\mathcal{F}\to \mathcal{E}$ が存在する。

直観的には、外延的直観主義高階論理(IHOL) の構文的モデル— つまり、型・項・証明の圏として構成される。

構成的性質

• 自由strictトポス$\mathcal{F}$ はトポスの2-圏においてbi-初始（[Forssell–Lumsdaine–Swan 2026, 命題1.22] / [Forssell–Lumsdaine–Swan 2026, 命題1.24]）
• Freydのグルーイング構成により、$\mathcal{F}$の終対象1は射影的 —これは存在性質 (EP) の圏論的対応物（[Forssell–Lumsdaine–Swan 2026, 命題1.24]）
• $\mathcal{F}$は階数付きトポスの余極限$\mathcal{F}\simeq {\mathcal{F}}_{\infty }={\mathrm{colim}}_{r\in N}{\mathcal{F}}_r$として表せる（コンパクト性、[Forssell–Lumsdaine–Swan 2026, 命題2.6]）

階数付きトポスとの関係

• 階数$\infty$ のトポス${\mathcal{F}}_{\infty }$ は自由トポスと圏同値（[Forssell–Lumsdaine–Swan 2026, 命題2.14]）。各階数$r$のトポス ${\mathcal{F}}_r$は有限階数の型のみを持つ「近似」。

関連ページ

• projectivity-of-N
• ranked-topos
• freyd-gluing
• michael-makkai

出典

• 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