自由トポス
自由トポス ℱ とは、トポスの2-圏における bi-初始対象。つまり、任意のトポス ℰ に対して一意な（同型を除いた）論理関手 ℱ → ℰ が存在する。
直観的には、外延的直観主義高階論理（IHOL）の構文的モデル — つまり、型・項・証明の圏として構成される。
構成的性質
- 自由 strict トポス ℱ はトポスの2-圏において bi-初始（命題 1.22 / 1.24）
- Freyd のグルーイング構成により、ℱ の終対象 1 は射影的 — これは存在性質 (EP) の圏論的対応物
- ℱ は階数付きトポスの余極限 ℱ ≃ ℱ_∞ = colim_{r∈N} ℱ_r として表せる（コンパクト性）
階数付きトポスとの関係
階数 ∞ のトポス ℱ_∞ は自由トポスと圏同値（命題 2.14）。各階数 r のトポス ℱ_r は有限階数の型のみを持つ「近似」。