The internal languages of univalent categories

技術要約：単価的圏の内部言語

問題提起
圏論的論理における内部言語定理は、構文（型理論）と意味論（圏モデル）の間の等価性を確立するものである。ClairambaultとDybjerによる画期的な結果[CD14]は、Seelyの元の定理[See84]を修正し、局所的にカルタン閉な圏（LCCC）の双圏と、外延的な恒等型、$\Sigma$型、および$\Pi$型を支持する民主的なコンテキスト付き家族（CwF）の双圏との間の双同値（biequivalence）を確立した。

しかし、この結果は集合論的基礎付けの中で定式化されていた。一価的基礎付け（ホモトピー型理論）において、標準的なCwFの概念は根本的な障害に直面する：一価性公理は、集合の型がそれ自体で集合ではない（それは1-typeである）ことを意味する。したがって、コンテキストにおける型の集まりが集合であることを要求するCwFの要件は、集合の単価的圏において違反される。さらに、「選ばれた」構造（例：分裂ファイブレーション）と「存在する」構造（例：同型を除いて極限）の区別は、集合論的基礎付けにおいては、選択公理や厳密化の手続きを必要とするコヒーレンス問題を生じさせる。一価的基礎付けでは、同型が恒等性と一致するため、これらの区別は消失するが、既存のCwFの枠組みは直接適用できない。

手法
本論文は、CwFではなく、単価的圏と**理解範疇（comprehension categories）**を利用して、一価的基礎付け内での新しい圏論的意味論の枠組みを開発する。

1. 単価的圏（Univalent Categories）: 著者は、対象の恒等型が同型（随伴同値）の型と等価である圏を扱う。これにより、随伴同値を恒等として扱うことが可能になり、構造（例：指数）の保存に関する証明が簡略化され、極限を選択するための選択公理の必要性が排除される。
2. 理解範疇（Comprehension Categories）: 型が集合であることを要求せずに依存型をモデル化するために、本論文は（ファイブレーションと表示された圏に基づく）理解範疇を採用する。理解範疇は、コンテキストの基底となる圏、型の表示された圏、クリービング（代入を提供）、および理解関手からなる。著者は、基底と表示された圏の両方が単価的である単価的完全理解範疇に注意を限定する。
3. 表示された双圏（Displayed Bicategories）: モデルの双圏の構成は、表示された双圏[AFM+21]に大きく依存している。このモジュール的なアプローチにより、著者はより単純な基底双圏の上に性質（例：有限極限、$\Pi$型、ユニバース）を層状に重ねることで、複雑な双圏（LCCCや位相圏など）を構築することができる。このモジュール性は、得られる双圏自体が単価的であることを証明することを容易にする。
4. 局所的性質（Local Properties）: 有限極限を持つ圏から、位相圏のようなより複雑な構造へと結果を拡張するために、著者はMaiettiの局所的性質[Mai05]の概念を適応させる。局所的性質とは、スライス（切断）の下で閉じている圏に関する条件である。著者は、得られる双圏の枠組み内でこれを形式化し、有限極限（基底ケース）から様々なクラスの位相圏への双同値を拡張する。
5. 再インデックス化とユニバース（Reindexing and Universes）: ユニバースの扱いについては、表示された双圏の再インデックス化を用いる。この手法により、基底となる圏から表示された圏へと双同値を転送することが可能になり、厳密な安定性法則を必要とせず、同型を除いて安定（単価的圏においては恒等となる）する特定の型形成（$\Sigma, \Pi$, 自然数）に対して閉じられたユニバースを定義できる。

主要な貢献
本論文は、主に4つの貢献を行う：

1. Clairambлоnt-Dybjerの単価的類似物: 著者は、有限極限を持つ単価的圏と、単価的完全民主的有限極限（DFL）理解範疇の間の双同値を構築する。これにより、有限極限を持つ単価的圏の内部言語が、unit、binary product、および$\Sigma$型を持つ外延的Martin-Lö効ド・ルーフェ型理論であることが確立される。
2. 局所的にカルタン閉な圏への拡張: 双同式は、$\Pi$型を支持するDFL理解範疇と単価的局所的にカルタン閉な圏へと拡張される。これは、単価的LCCCの内部言語が$\Pi$型を持つ外延的Martin-Löf型理論であることを確認するものである。
3. 位相圏とユニバースへの拡張: 局所的性質を用いて、様々なクラスの位相圏（前位相圏、$\Pi$-前位相圏、初等位相圏、および自然数オブジェクトを持つ位相圏）へと一般化する。さらに、著者はこれらの圏において特定の型形成（自然数、部分対象分類子、命題のリサイズ、$\Sigma$型、$\Pi$型）に対して閉じられたユニバースを定義し、ユニバースを持つ初等位相圏の双同式を確立する。
4. 形式化: すべての構成と証明は、UniMathライブラリを用いたRocq証明助手において形式化されており、正当性を保証し、理論の機械検証可能な参照を提供している。

結果
本論文は、様々なクラスの単価的圏について、対応するクラスの単価的理解範疇との間に双同式が存在することを証明する。具体的には以下の通りである：

• 有限極限: 単価的有限極限圏 $\simeq$ DFL理解範疇 (Unit, Product, Equalizer, $\Sigma$)。
• LCCC: 単価的LCCC $\simeq$ $\Pi$型を持つDFL理解範疇。
• 位相圏: 単価的初等位相圏（NNOの有無にかかわらず） $\simeq$ 対応する局所的性質（例：部分対象分類子、非連結和、商）を持つDFL理解範疇。
• ユニバース: 特定の型形成に対して閉じられたユニバースを持つ単価的初等位相圏 $\simeq$ 対応する閉包条件を満たすユニバース対象を持つDFL理解範疇。

本論文は、様々なクラスの単価的圏において、その内部言語が外延的Martin-Löf型理論であることを示している。単価的圏の使用は、分裂ファイブレーションの必要性を排除し、以前の集合論的モデルにおいて（代入が厳密に成立しなければならないために）問題を惹起していたコヒーレンスの問題を、同型が恒等であることにより解決し、理論を簡素化する。

意義と主張
本論文は、その展開が依存型理論の意味論に対する新しい視点を提供すると主張している。単価的圏を利用することで、著者は、健全性を確保するために集合論的基礎付けで必要とされる分裂ファイブレーションや選択公理の技術的なオーバーヘッドを回避している。単価的基礎付けに固有の構造恒等原理は、対象が厳密な等号ではなく同値を除いて識別される、より自然な圏論的構造の扱いを可能にする。

著者は、本研究において構文や初期モデルを構築しているのではなく、むしろ内部言語定理の圏論的な側面（モデル間の等価性）に焦点を当てていることを明示している。理解範疇は単価的基礎付けに適しているが、他の構造（例えばCwF）は、型の集合制限のために適していない。本論文は、適切な構文（例えば群群構文）とその解釈の開発を将来の課題として残しつつ、基礎的な一歩を築くものである。その意義は、単価的圏論的構造と型理論との間の、堅牢で機械検証可能な対応関係を確立し、単価的基礎付けが、以前の集合論的な定式化に見られた欠陥なしに、これらの内部言語定理を自然に支持することを示した点にある。