Freyd グルーイング
トポス理論における標準的な手法。トポス ℰ を ℰ↓Γ（ℰ の箭圏、または ℰ と Set の貼り合わせ）に埋め込むことで、ℰ の対象に「集合論的な情報」を付加する。
自由トポスにおける役割
- Freyd グルーイングの古典的応用: 自由トポス ℱ の終対象 1 が射影的であることの証明。これが存在性質（EP）の証明となる。
- 内部 Freyd グルーイング（定理 4.21）: 任意のトポス ℰ において、内部自由 r-トポス 𝔽_r の終対象は（indexed-）射影的。
- これを有限階数 r ごとに適用し → 標準解釈で外部化 → N の射影性を得る、というのが Makkai 証明の核心戦略。