Univalent Enriched Categories and the Enriched Rezk Completion

技術要約：単価的濃密圏（Univalent Enriched Categories）と濃密Rezk完備化

問題提起
圏論は数学および計算機科学における基礎的な枠組みであり、濃密圏（enriched categories）は高次圏論、ホモトピー論、および効果的な言語のセマンティクス（例：DCPOを用いた効果的な言語）において重要な役割を果たしている。しかし、単価的基礎（Univalent Foundations / HoTT）の文脈において、標準的な圏の定義は「同型な対象は区別できない」という等価性の原理を満たさないことが多い。「単価的圏（univalent categories）」（対象の同一性が同型性と等価である圏）は通常の圏については確立されているが、単価的濃密圏の理論は未だ発展途上である。具体的には、構造同一性原理（structure identity principle）、等価性の特徴付け、およびRezk完備化（単価的反映）の存在に関する形式化された結果が不足している。さらに、クレイスリ圏（Kleisli categories）のような標準的な構成は単価的にならないことが多く、濃密な設定において単価的な類似物を構築するための手法が必要とされている。

手法
本論文では、UniMathライブラリを用い、単価的基礎に従ってRocq証明助手内で濃密圏の理論を展開する。核となる手法は以下の通りである：

1. 構造としての濃密化: 濃密圏を（Kellyによる定義のように）対象とホム対象の集まりとして定義するのではなく、単なる「圏に付随する濃密化」として定義する。濃密化とは、単元モノイダル圏 $\mathcal{V}$ におけるホム対象、恒等射および合成射、そして圏の射とホム対象の要素との間の対応からなる。この視点は、濃密圏を「追加の構造を持つ単価的圏」として扱うものである。
2. 表示双圏（Displayed Bicategories）: 構造同一性原理を証明するために、表示双圏のメカニズムを利用する。著者らは、単価的圏の双圏（$UnivCat$）上の表示双圏$dEnrichCat_{\mathcal{V}}$ を定義する。この表示の全双圏（total bicategory）は $EnrichCat_{\mathcal{V}}$ である。これにより、$UnivCat$ の既存の単価性に関する結果を再利用して、濃密な設定における単価性を証明することが可能になる。
3. 直交分解系: 等価性を特徴付けるために、双圏における直交分解系を用いる。著者らは、充満忠実かつ本質的に全射な濃密関手を定義し、それらが直交分解系を形成することを証明する。
4. 2つのRezk完備化の構成: 濃密圏のRezk完備化について、2つの異なる構成法を提示する：
   • イェンデンの埋め込み: 完備化を濃密イェンデンの埋め込みの像として構成する。これには $\mathcal{V}$ が完備かつ対称モノイダル閉である必要があるが、標準的な圏論に依拠している。
   • 高次誘導型（Higher Inductive Types: HITs）: HITsの除去規則を用いて、基礎となる圏のRezk完備化に濃密化を付与することで完備化を構成する。このアプローチは $\mathcal{V}$ の完備性や閉性を仮定せず、宇宙がHITsの下で閉じている場合に宇宙レベルを保持する。
5. 普遍性: Rezk完備化の普遍性を確立し、弱等価（充満忠実かつ本質的に全射な関手）による前合成が関手圏の随伴等価を誘導することを示す。

主要な貢献と結果

• 構造同一性原理: 本論文は、単価的濃密圏の双圏（$EnrichCat_{\mathcal{V}}$）が単価的であることを証明する（定理2.8）。これは、2つの単価的濃密圏の間の同一型が、それらの間の随伴等価の型と等価であることを意味する。
• 等価性の特徴付け: すべての充満忠実かつ本質的に全射な濃密関手が随伴等価であることを証明する（定理4.8）。この結果は構成的であり、選択公理に依存せず、ドメインとコドメインが単価的であることを前提としている。
• Rezk完備化: 濃密圏のRezk完備化のための2つの構成法を提供する（構成5.5および5.7）。すべての濃密圏がRezk完備化を持ち、任意の関手が弱等価に沿って一意に拡張するという普遍性を満たすことを証明する（定理5.2）。
• 単価的クレイスリ圏: 単価的な濃密クレイスリ圏を構成する。標準的なクレイスリ圏 $K(T)$ と、その単価的な対応物 $Kleisli(T)$ （アイレンバーグ・ムーア圏の充満部分圏として）を定義する。Rezk完備化と普遍性を用いることで、$Kleisli(T)$ が単価的濃密圏の双圏におけるクレイスリ対象の普遍性を満たすことを示す（構成6.9）。
• 例と特徴付け: 自己濃密化、反対濃密化、および基底の変更を含む多数の例を提供する。カルテジアン構造（DCPOなど）上の濃密化を特徴付け、点付き集合やポセットを扱うための「スマッシュ積をサポートする閉構造」の概念を導入するが、点付きDCPOに関する制限についても言及している。

意義と主張
本論文は、単価的基礎における濃密圏論の堅牢な基礎を確立することを主張している。その主な意義は以下の通りである：

1. 形式化: 以前は通常の圏と比較して形式化が進んでいなかった濃密圏のための、Rocq/UniMathにおける形式化ライブラリを提供したこと。
2. 概念の正当性: 濃密圏を（濃密化を介した）単価的圏とみなすことが、構造同一性原理のような基本性質の証明を簡素化することを実証したこと。
3. 非単価性の解決: クレイスリ圏のような一般的な構成が本質的に単価的ではないという問題に対し、必要な普遍性を保持する単価的なバージョンを得るための体系的な方法（Rezk完備化）を提供することで対処したこと。
4. 基礎的ツール: 単価的濃密圏の双圏を単価的双圏として確立したことは、単価的な設定におけるさらなる内部圏論（例：モナド、極限）を展開するための前提条件である。

著者らは、自身のアプローチが多くの標準的なケースをカバーしている一方で、適切な圏内での商を取る必要がある構造（点付きDCPOなど）におけるスマッシュ積に関しては制限があることを述べている。今後の課題として、濃密圏の道具立ての開発や、これらのケースを扱うためのスマッシュ積の概念の一般化などが挙げられている。