Extension Types for Free

技術的要約：自由な拡張型としての拡張型：2レベル型理論におけるコファイブレーション、接着、および一価性

問題提起
拡張型（Extension types）は依存型理論における基本的な概念であり、様々な文脈（固定された端点を持つパスとしての立方型理論、部分的な形状上の項を持つRiehlとShulmanの単体型理論、あるいは制御された展開メカニズムなど）で現れる。既存の枠組みでは、これらの型は通常、その形成と規則を規定するメタ理論的な「フェイス計算（face calculus）」または「形状層（shape layer）」によって制御される新しいプリミティブとして仮定される。このアプローチは、規則を検証するために、特定のモデル構成や公理的追加（厳密な境界条件、相対的な関数外延性、ホモトピー拡張性質など）を必要とすることが多い。ホモトピー型理論（HoTT）における中心的な未解決問題は、「Book HoTT」（HoTT Bookにおける公理的定式化）と立方型理論との間の正確な関係、特に両者が互いに保守的な拡張であるかどうかを判断することである。

手法
本論文は、統一的な枠組みとして**2レベル型理論（2LTT）**を利用する。2LTTは、一意性（UIP）と関数外延性を満たす「厳密な（outer）」等価レベルを備えたHoTTを、標準的なホモトピー構造を保持する「内的な（inner/fibrant）」レベルへと強化したものである。

• 意味論: この枠組みは意味論的に「自由（free）」である。Hoottの標準的なモデル（例：単体集合、立方集合）は、前層構成を通じて自動的に2LTTのモデルとなる。この理論は内的なレベルに対して保守的であり、内的な言語において、HoTTですでに証明可能であったものではない新しい定理が証明されることはない。
• 拡張型の定義: 拡張型を仮定する代わりに、本論文では2LTTの内部でこれらを定義する。コファイブレーション $i: \Phi \hookrightarrow \Psi$（outerレベルにおける写像）、$\Psi$ 上のファイブラントな族 $A$、および部分的な切断 $a$ が与えられたとき、拡張型は制限写像の**厳密なファイバー（strict fiber）**として定義される：
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  ここで、$=_s$ はouterレベルの厳密な等価を表す。
• コファイブレーション: 「フェイス計算」は、outerレベルにおけるコファイブレーションのクラスへと置き換えられる。本論文では、どの写像をコファイブレーションとするかという具体的な選択をパラメータとして扱うことで、コアとなる定義を変更することなく、異なる設定（単体、立方など）に適応できる枠組みを提供している。

主要な貢献と結果

1. 「自由な」拡張型:
   本論文は、2LTTにおいて、RiehleとShulmanが提案した拡張型の計算全体が、仮定されるものではなく定義可能であることを示している。

• 厳密な規則: 導入、除去、$\beta$、$\eta$、および境界の規則は、構成によって厳密に成立する。
• 証明可能な公理: 他の設定で仮定される公理（相対的な関数外延性やホモトピー拡張性質（realignment）など）は、2LTTにおけるコファイブレーションとファイブレーションの性質から導かれる定理となる。
• 統一: この単一の定義は、立方体のパス、Riehle-Shulmanの拡張型、および命題にインデックスされた型（制御された展開）を含む、既存の様々な事例を包含する。

2. 接着（Gluing）と一価性（Univalence）の同値性:
   本論文は、2LTTの枠組みにおける、立方的な接着（cubical gluing）と一価性公理を結ぶ正確な含意のサイクルを確立する：

• 一価性 $\implies$ 接着: 内的なユニバースが一価的であれば、任意のコファイブレーションに対して、「Glueデータ」（Glue型を形成するために必要な構造）の型は**可縮（contractible）**である。これは、ホモトピー形式で規則を満たすGlue構造が存在することを意味する。
• 接着 $\implies$ 一価性: 「弱いGlue構造」（境界の一致に内的な等価のみを必要とし、パス区間構造を持つもの）の存在は、ユニバースが一価的であることを意味する。
• 結果: パス区間が存在する場合、一価性とGlueデータの可縮性は同値である。これは、標準的な含意の方向（Glue型がUnivalenceを導くという方向）を逆転させ、双方向の同値性を確立するものである。

3. 形式化:
   セクション2からセクション5のすべての結果は、--two-level フラグを用いてAgdaで自動形式化されている。この形式化は、内的なHoTTの議論と、厳密なレベルに関する外的な推論を組み合わせ、理論的主張の整合性と正当性を検証している。

4. 保守性へのアプローチ:
   立方型理論がBook HoTTに対して保守的であるかどうかという未解決問題に対処するための戦略を、本論文は提案している。両方の理論を2LTTの中に表現することで：

• Book HoTTは、MLTT + Univalence（内的なレベル）として表現される。
• 立方型理論は、ML列 + Glue + パス区間（outer/構造的な仮定）として表現される。
  本論文は、パス区間を持つ基底理論の上で、Univalence公理とGlue公理が相互に導出可能であることを証明している。これは、両理論の核心的な違いが論理的なものではなく、構造的なものである可能性を示唆しており、保守性の証明への道筋を提供している。

意義と主張
本論文は、2LTTの枠組みが拡張型のための「自由」かつ一様な基礎を提供し、その規則を検証するためにアドホックな公理や特定のモデル構成を必要としないことを主張している。フェイス計算をコファイブレーションとして内部化することで、本理論は文献に見られる様々な拡張型の事例を統一している。

立方型理論とBook HoTTの関係については、本論文は控えめな立場をとっている。保守性の予想を解決したと主張しているのではない。代わりに、それは**概念実証（proof of concept）**を提供している。すなわち、2LTTの視点を通じることで、立方型理論の核心的なメカニズム（Gluing）が、HoTTの核心的な公理（Univalence）と論理的に同値であることを示している。この同値性により、研究者は構造的な拡張（Glue型など）を公理的な拡張へと一つの枠組みの中で翻訳することが可能となり、比較を容易にし、将来的な保守性の証明への道を切り開く。論文では、完全な同値を達成するために、Hoott側における「パス区間」の仮定を解消することが依然として課題であると明記されている。