The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

技術要約：ホモトピー型論におけるライプニッツ随伴

問題提起
シンプリシャル型論（STT）は、区間（interval）を用いて型に方向性を持つ射を付与することで、ホモトピー型論（HoTT）を拡張し、高次圏のための合成的な枠組みを提供する。中心となる課題は、「セーガル型（Segal types）」、すなわち方向性を持つ射が合成可能であるような型を定義することである。合成自体は単純であるが、この合成が結合律および単位律を満たすことを保証するには、無限の階層的な高次コヒーレンスが必要となる。RiehlとShulmanによる標準的なSTTの定式化では、これらのコヒーレンスはしばしばメタ理論的な構成によって扱われるため、完全な形式化を困難にしている。具体的には、$(2,1)$-ホルンに対する一意の充填を持つ型（セーガル型の基本条件）が、すべての内側$(n,k)$-ホルンに対する一意の充填（合成の結合律や単位律を一般化したもの）を導出することを証明することは、非自明である。先行研究（RiehlおよびShulmanによるもの）では、特定の低次元ケース（$n=3$）はカバーされていたが、統一されたHoTTの枠組み内で、すべての$n$および$k$に対して一般的に成立する証明は、未解決の技術的障壁として残されていた。

手法
著者らは、RiehlとShulmanのメタ理論的な区間アプローチではなく、Gratzer、Weinberger、およびBuchholtzに従った「プレーン（plain）」なホモトピー型論のアプローチを採用している。彼らは、全順序や特定のモダリティを必要としない、有界分配束を形成する区間型 $I$ を仮定している。

核心となる技術的革新は、「ワイルドな型の圏（wild category of types）」における**ライプニッツ随伴（Leibniz adjunction）**の内在化である。

1. ワイルドな圏: 著者らは、「ワイルドな圏」を扱う。これは圏論をHoTTへと素朴に翻訳したものであり、これらは高次のコヒーレンス・データ（結合律や単位律が定義的に成立するか、あるいは追跡されない）を欠いているため、$(\infty, 1)$-圏とは区別されるが、著者の目的には十分である。
2. 随伴: 彼らは、写像のワイルドな圏において、押し出し積（pushout-product）（$\hat{\times}$ で表記）がプルバック・ホム（pullback-hom）（$\pitchfork$ で表記）の左随伴であることを確立している。
   • 写像 $f: A \to B$ と $g: X \to Y$ に対して、押し出し積 $f \hat{\times} g$ は、$f \times Y$ と $A \times g$ の押し出しから誘導される写像である。
   • プルバック・ホム $f \pitchfork g$ は、関数型間の誘導された写像である。
   • この随伴は、$\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$ を満たす。
3. 写像 vs ファミリー: 写像のワイルドな圏におけるこの随伴の直接的な証明は、コヒーレンス・データの追跡（7つの写像と識別子の組）の複雑さゆえに困難である。これを克服するため、著者らは一価性公理（univalence axiom）を利用して、写像のワイルドな圏とファミリー（依存型）のワイルドな圏との間の同値性を確立している。彼らは、押し出し積とプルバック・ホムが、ファミリーの圏におけるファイバーごとのジョイン（fiberwise join）および特定の依存積構成に対応することを証明しており、そこでは随伴の検証がより容易になる。

主要な貢献と結果

1. ライプニッツ随伴 (定理 3.16): 本論文は、押し出し積とプルバック・ホムが型のワイルドな圏において随伴対を形成することを証明している。これは、1-圏ではよく知られていることであるが、高次構造（たとえ「ワイルド」な設定であっても）においてこれを証明するには、写像とファミリーの間の同値性を慎重に扱うことで、扱いづらいコヒーレンス・簿記を回避する必要があるため、重要な技術的成果である。
2. セーガル型の性質の一般化 (定理 4.9): ライプニッツ随伴を用いることで、ある型が $(2,1)$-ホルンに対する一意の充填を持つ（すなわち、セーガル型である）ならば、それが自動的にすべての内側 $(n,k)$-ホルン ($0 < k < n$) に対する一意の充填を持つことを証明している。
   • これは、RiehlとShulmanの結果（$n=3$をカバーしていた）を一般化し、Lurieの結果のシンプリカル型論版を提供するものである。
   • 証明は、内側ホルンの包含 $\lambda^n_k$ が「内側アノダイン（inner anodyne）」（すなわち、すべてのセーガル型に対して左直交である）であることを示すことに依拠している。これは、$\lambda^n_k$ が押し出し積 $\lambda^n_k \hat{\times} \lambda^2_1$ のレトラクトであることを示し、次にライプニッツ随伴から導かれる直交性の閉包特性を適用することによって達成される。
3. 形式化: すべての結果は Cubical Agda で形式化されている。コードは公開されており、インデックスや押し出しに関する複雑な組合せ論的議論の検証として機能する。

意義と主張
本論文の主要な貢献は、ライプニッツ随伴をHoTT内に内在化することに成功し、それがシンプリカル型論における高次コヒーレンスを導出するための強力なツールとなることを示した点にあると主張している。

• 合成的な枠組み: 内部的な区間型を用いることで、セーガル型に関するすべての高次コヒーレンスを、メタ理論的な量化に頼ることなく、Hoots内で合成的に記述し導出できることを示している。
• 形式化の実現可能性: 著者らは、自身のアプローチがAgdaでの完全な形式化を可能にすることを強調している。彼らは、Riehl–Shulmanのメタ理論的アプローチは（メタレベルでの集合論的な推論により）定理の「表明」を容易にするかもしれないが、彼らの内部的な枠組みにおける一般ケースの「証明」は非自明であり、コヒーレンス・トラッキングに関する「圧倒的な大部分の困難」を管理するためにライプニッツ随伴の開発が必要であったと述べている。
• 技術的有用性: 写像とファミリーのワイルドな圏の間の同値性は、押し出し積とプルバック・ホムを含む証明を簡略化するための極めて重要な方法論的ツールとして提示されており、これにより直交性の性質の導出が可能となっている。

要約すると、本論文は、ライプニカル随伴をワイルドな圏の設定において適用することを通じて、セーガル型の基本的な条件が完全な高次圏的コヒーレンスを導出することを証明し、シンプリカル型論の厳密に形式化された基礎を提供するものである。