Strict stability of extension types

技術要約：拡張型の厳密な安定性

問題提起
本論文は、RiehlとShulmanによって導入されたホモトピー型論（HoTT）における$(\infty, 1)$-圏の合成的発展における、基礎的な欠落に対処するものである。このシステムの意味論は、単体的ホモトピー論とSegal空間モデルを用いてスケッチされたが、元の定式化では、拡張型（extension types）の厳密な安定性（strict stability）、すなわち置換の下での安定性を実証する点が未解決のまま残されていた。型理論的モデルにおいて「厳密な安定性」とは、型形成（extension typesのようなもの）の解釈が、単なる同型やホモトピーとしてではなく、プルバック（置換）と厳密に可換であることを要求する。この性質がなければ、特定の内部圏論（例えばMartini–Wolfによるもの）が要求する厳密な等価性をサポートするような形で、システムを$\infty$-toposの内部言語として完全に解釈することができない。

手法
著者は、Voevodskyによって記述され、後に局所的なユニバースに対してLumsdaineとWarrenによって一般化された**分割法（splitting method）**を採用している。このアプローチは、以下の技術的なステップを含む。

1. ユニバース・カテゴリー： 本研究は、ユニバース対象$U$と普遍的なファイブレーション$\pi: \tilde{U} \to U$を備えたユニバース・カテゴリー（$\mathcal{C}$）の中に位置づけられる。著者は、「分割（splitting）」、すなわちユニバーサル・ファイブレーションに対するプルバック正方形のグローバルな選択が存在することを仮定している。これにより、再インデックス化（置換）が、単なる同型ではなく、対象と射の厳密な等価性によってモデル化されることが保証される。
2. 生成的コンテキスト（Generic Contexts）： Awodeyの自然モデルに関する研究のスタイルに従い、本論文は拡張型の形成および導入のための生成的コンテキスト（分類対象）を定義する。
   • $U_{\text{Ext}@j}$は、形状の包含関係$j: \phi \hookrightarrow \psi$に対する型族$A$と部分切断$a$のペアを分類する対象として定義される。
   • $U_{\lambda@j}$は、完全な拡張$b$を持つトリプル$\langle A, a, b \rangle$を分類する対象として定義される。
3. 厳密なプルバック構成： 著者は、拡張型形成の形式である$\text{Ext}@j$と、導入写像$\lambda@j$を、これらの生成的コンテキストとユニバースの間の射として構成する。分割を利用することで、論文はこれらの写像によって形成される正方形が（弱いプルバックではなく）**厳密なプルバック（strict pullback）**であることを証明する。
4. ファイブリティ（Fibrancy）の仮定： 標準的なモデル（$\infty$-toposにおける単体的対象）への適用可能性を維持しつつ、技術的な設定を簡略化するため、著者は「形状」（単体的コンテキスト）がファイブラントであることを仮定している。これにより、Leibnizコテンソルがファイブレーションとなることが保証され、拡張型が通常の1-圏的なプルバックとしてモデル化されることが可能になる。

主要な貢献と結果
主要な貢献は、拡張型の厳密な安定性を確立する定理3.8である。この定理は、型理論的モデル・トポス$\mathcal{E}$とその関連する単体的モデル$s\mathcal{E}$に対し、標準的な型形成の固定された分割を用いることで、任意のコンテキスト射$\sigma: \Delta \to \Gamma$に対して以下の厳密な等式を満たす拡張型の解釈が得られることを証明している：

1. 形成の安定性： $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. 導入の安定性： $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. 除去の安定性： $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

さらに本論文は、分割によって定義されたプルバック正方形の普遍的性質に依拠することで、$\beta$-および$\eta$-計算規則がこの厳密に安定した枠組みの中でどのように満たされるかを詳述している。

意義と主張
本論文は、この結果がRiehl–Shulmanのシステムにおける拡張型の厳密な安定性に関する未解決問題を解決することを主張している。実用的な帰結として、このシステムは、$\infty$-toposの単体的対象における堅牢な意味論を備えることになる。これにより、内部圏論（Martini–Wolfによるもの）の文脈において、厳密な安定性が型理論的操作と圏論的なプルバックを完全に一致させるため、当該のシステムを用いて内部$\infty$-圏に関する定理を証明することが可能となる。

著者は、技術的な簡略化のために単一のユニバースとファイブラントな形状を仮定しているものの、その推論は、本質的な障害なしにユニバースの階層やより複雑なファイバー構造へと一般化できると考えている。本研究は、単体的HoTTの合成的構文と、$\infty$-toposの厳密な意味論との間の架け橋として機能する。