算術宇宙
定義: 算術宇宙（AU）とは、リスト付き余完備前トポス（list-arithmetic pretopos）— すなわち、余完備性（有限余極限）とパラメータ化リスト対象を持つ局所有限余完備圏（locos）であって、さらに exact なもの。
トポスより弱い構造で、冪対象（power-object）を仮定しない。その代わりにリスト対象（自然数や帰納的データ型に対応）を持つ。
重要性
- 算術宇宙上の内部トポス: 任意の算術宇宙 ℰ は、内部言語で記述された初期内部 strict r-トポス 𝔽_r を持つ（定理 3.23）
- AU-論理関手はこの内部トポスを保存する
- Gödel 番号付け（系 3.35）: 各内部 r-トポスの各型は AU 内で可算（enumerable）
これにより、圏論的内部化（cirernalization）が可能になり、有限階数の近似をトポス内部で扱えるようになる。