論文「Homotopy Type Theory におけるコスライス余極限」の技術的サマリー

Perry Hart と Kuen-Bang Hou (Favonia) によるこの論文は、ホモトピー型理論（HoTT）の枠組み内において、コスライス圏（coslice categories）における余極限（colimits）、特に**コスライス余極限（coslice colimits）**の理論を構築・分析することを目的としています。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題設定と背景

HoTT において、高次帰納型（HITs）は余極限として理解されることが一般的です。特に、ある宇宙 $\mathcal{U}$ 内の型 $A$ に対するコスライス圏 $A/\mathcal{U}$（$A$ から出る射を持つ型たちの圏）における余極限は、** pointed types（点付き型）の圏や高次群（higher groups）**の圏における構成に不可欠です。

従来のアプローチでは、HITs を公理として仮定するか、一般的な HIT のスキーマを用いて $A/\mathcal{U}$ 内の余極限を定義することができました。しかし、これでは通常の宇宙 $\mathcal{U}$ 内の余極限とコスライス圏 $A/\mathcal{U}$ 内の余極限の間の構造的な関係が明確になりませんでした。

本研究の核心的な問いは以下の通りです：

• $A/\mathcal{U}$ 内の余極限を、$\mathcal{U}$ 内の既存の余極限（pushout や coproduct など）を用いて具体的に構成できるか？
• その構成を通じて、$A/\mathcal{U}$ 内の余極限が持つ性質（例えば、接続性の保存や、直交分解系との相互作用）をどのように導き出せるか？

2. 手法と主要な構成

著者らは、Martin-Löf 型理論（MLTT）に pushout を追加したシステム（MLTT + Colim）を用いて、$A/\mathcal{U}$ 内の余極限を明示的に構成しました。

2.1. 主となる構成（Main Connection）

セクション 5.4 で提示される「主となる接続（main connection）」が本論文の核心です。
$A/\mathcal{U}$ 内の図式 $F$ の余極限を構成する際、以下の手順を踏みます：

1. まず、図式 $F$ の基底となる $\mathcal{U}$ 内の図式 $F_g$（忘却関手による射影）の通常の余極限 $\text{colim}(F_g)$ を取ります。
2. 次に、コスライス構造（$A$ からの射）を反映するために、$\text{colim}(F_g)$ 上に特定の「区別されたループ（distinguished loops）」を埋め込むための 2-セル（ホモトピー）を付加します。
3. この操作は、$\text{colim}(F_g)$ と定数図式 $A$ の pushout を取ることで実現されます。具体的には、$\text{colim}(F_g)$ から $A$ への射と、$A$ から $\text{colim}(F_g)$ への射（定数図式からの射影）を結びつける pushout を構成します。

この構成により、$A/\mathcal{U}$ 内の余極限は、$\mathcal{U}$ 内の余極限と pushout の組み合わせとして記述可能になります。

2.2. 忘却関手による余極限の生成

この構成を用いて、忘却関手 $F_g: A/\mathcal{U} \to \mathcal{U}$ がツリー（contractible graph）上の図式に対して余極限を「生成（creates）」することを証明しました。

• 定理: $\Gamma$ がツリーである場合、忘却関手 $F_g$ は $A/\mathcal{U}$ 内の余極限を保存し、かつ反映します（Corollary 5.4.6）。
• これは、局所的にカルテシアン閉（LCC）な $\infty$-圏のコスライスが必ずしも LCC ではないという古典的な知見に対し、ツリー上の図式に限れば余極限の普遍性が保持されることを示しています。

2.3. 直交分解系との相互作用

セクション 7 では、直交分解系（Orthogonal Factorization Systems, OFS）との関係を分析しました。

• 宇宙 $\mathcal{U}$ 上の OFS において、左クラスに属する射（例えば $n$-connected な射）は、$A/\mathcal{U}$ 内の余極限によっても保存されます。
• この結果は、**高次群（higher groups）**の圏が余完全（cocomplete）であることを示すために利用されました。

3. 主要な結果

3.1. 高次群の圏の余完全性

著者らは、Buchholtz, van Doorn, Rijke によって定義された「$k$-重に群化された $n$-groupoid（$(n, k)\text{GType}$）」の圏が、グラフ上の図式に対して余完全であることを証明しました（Section 7.1）。

• 具体的には、点付き $n$-connected 型の図式の余極限は再び $n$-connected であり、かつ適切な切断（truncation）を施すことで高次群の圏内で完結します。
• これにより、高次アーベル群などの圏における余極限の存在が保証されました。

3.2. コホモロジー理論への応用

セクション 8 では、コホモロジー理論（Eilenberg-Steenrod cohomology）が有限余極限を「弱極限（weak limits）」に写すことを示しました。

• Mayer-Vietoris 系列と、セクション 5.5 で得られた「コプロダクトの pushout による構成」を用いることで、有限グラフ上の余極限に対するコホモロジーの振る舞いを解析しました。
• 内部の選択公理を仮定すれば、コホモロジーは有限余極限を集合の圏における弱極限（全射な極限）として扱います。これは Brown 表現定理の証明における重要な条件と一致します。

3.3. 普遍性（Universality）

セクション 6 では、ツリー上の図式に対するコスライス余極限が普遍性（pullback-stable）を持つことを示しました。これは、局所的にカルテシアン閉な圏の性質を、コスライス圏の特定の部分で再確認する結果です。

4. 形式化

本論文の主要な部分（特にセクション 5.4 のコスライス余極限関数の構成、忘却関手による生成、直交分解系の保存など）は、Agda によって形式化されています。

• 形式化ライブラリは [7] として参照されており、論文の主張の厳密性を保証しています。

5. 意義と結論

この論文の意義は以下の点に集約されます：

1. 構成論的アプローチの確立: 高次帰納型（HITs）を公理的に扱うのではなく、Pushout や通常の余極限を用いて明示的に構成することで、HoTT 内の圏論的構造をより深く理解可能にしました。
2. 圏論的性質の一般化: 宇宙 $\mathcal{U}$ 上の性質（接続性、直交分解系）が、点付き型や高次群の圏（コスライス）にどのように拡張されるかを体系的に示しました。
3. 高次群の圏論的基礎: 高次群の圏が余完全であるという結果は、代数的トポロジーにおける高次構造の計算を HoTT 内で厳密に行うための基盤を提供します。
4. コホモロジーとの統合: 余極限とコホモロジーの相互作用を、HoTT の内部で弱極限の観点から再解釈し、古典的な位相幾何学の結果（Brown 表現定理の条件など）との整合性を示しました。

総じて、この研究は HoTT における圏論的構成（特に余極限）の理論的基盤を強化し、合成ホモトピー理論（synthetic homotopy theory）の発展に寄与する重要な成果です。