The $\infty$-category of $\infty$-categories in simplicial type theory

技術的要約：Simplicial Type Theoryにおける$\infty$-categoryの$\infty$-category

問題提起
RiehlとShulmanによって導入されたSimplicial Type Theory (STT) は、有向区間 $I$ を用いてHomotopy Type Theory (HoTT) を拡張することにより、$(\infty, 1)$-category理論のための合成的な枠組みを提供する。STTは、$\infty$-categoryを特定の性質（Segal条件およびRezk条件）を満たす型として定義し、極限、余極限、およびファイバー付き圏の構成をサポートすることに成功しているが、基礎的なギャップが残っていた。具体的には、型 $U$ 自体がSTT内において$\infty$-categoryにはならないという点である。すなわち、$\infty$-categoryの述語（$\text{isCat}$）を満たす型の部分型は、合成的な射（関数 $I \to \sum_{A:U} \text{isCat}(A)$）が合成不可能であったり、関手を忠実に表現できなかったりするため、カテゴリーを形成できない。その結果、「カテゴリーのカテゴリー」（$\text{Cat}$）は、宇宙の構成可能な部分型として予想されてはいたものの、実現されていなかった。この欠如により、straightening–unstraightening定理の内部化が妨げられ、有向型理論を高次代数構造へ適用することが困難となっていた。

手法
著者らは、cubical type theoryおよびmodal dependent type theory (MTT) の手法をSimplicial Type Theoryに適応させることで、$\text{Cat}$を構築する。その手法は以下の主要なステップで進行する：

1. Triangulated Type Theory ($TT^\triangle$): 著者らは、有向区間 $I$ が全順序集合ではなく有界分配束であるSTTの緩和版である$TT^\triangle$内で作業を行う。このモデル（Dedekind cubical spaces）は、指数関数ファンクタ $I \to (-)$ に対する「驚くべき右随伴（amazing right adjoint）」を許容する。これは標準的なsimplicial spaceには欠けている特徴であり、普遍的なファイブレーションを定義するために極めて重要である。
2. モダリティ: 理論は、$\flat$ モダリティ（離散ファンクタ）および $\sharp$ モダリティ（余離散ファンクタ）を含むモダリティによって拡張される。これらにより、大域的要素の内在化、および離散的な群（groupoid）と一般的なカテゴリーの区別が可能となる。
3. Universal Cocartesian Family: Licataら、およびWeaverとLicataに従い、著者らは$\text{Cat}$を型に対する直接的な述語によってではなく、universal cocartesian familyの基底として定義する。彼らは、$I^n$ 上で定義された述語（内的なファイブレーションであることや、局所的にcocartesian liftを持つことなど）を、宇宙 $U$ 上の述語へと転置するLemma 2.9を利用する。
4. $\text{Cat}$ の定義: $\text{Cat}$ は、Rezkであり、inner（相対的なSegal条件を満たす）であり、かつ合成可能なlocally cocartesian liftを持つ型からなる $U$ の部分型として定義される。
5. Directed Univalence: 著者らは、$\text{Cat}$ が「directed univalence」原理を満たすことを証明し、$\text{Cat}$ における合成的な射と、基礎となる型の間の関手の間の等価性を、$\flat$ モダリティを介して確立する。

主要な貢献と結果

• $\text{Cat}$ の構築: 主要な貢献は、STT内における$\infty$-categoryの$\infty$-categoryの最初の構築である。著者らは$\text{Cat}$を宇宙の部分型として定義し、それが自身もカテゴリーであること（すなわち、simplicial、Segal、およびRezkであること）を証明する。
• 普遍的性質 (Theorem 4.2): 本論文は、$\text{Cat}$ がuniversal cocartesian familyの基底であることを確立する。任意のカテゴリー $C$（具体的には$\flat$-annotatedなもの）に対して、以下の等価性が成立する：
  \langle \flat \mid C \to \text{Cat} \rangle \simeq \langle \flat \mid \sum_{E: C \to U} \text{isCocart}(E) \end{rangle
  これは、Grothendieck対応（straightening–unstraightening）を純粋に型理論的に特徴付けるものである。
• Directed Univalence (Corollary 5.5): 著者らは、$\text{Cat}$ の $\flat$-要素 $A, B$ について、合成的な射の型がそれらの間の関手の型と等価であることを証明する：
  $$\text{hom}_{\text{Cat}}(A, B) \simeq \langle \flat \mid A \to B \rangle$$
  この結果は、等価性が $\flat$ モダリティなしで成立する空間のカテゴリー（離散的なカテゴリー）と、$\text{Cat}$ とを区別するものである。
• Synthetic Straightening–Unstraightening: Unstraightening 写像 $U: (C \to \text{Cat}) \to \text{Cat}/C$ のファイバーを分析することにより、著者らはLurieのstraightening–unstraightening定理の完全な合成的な証明を提供する。彼らは、この写像の像がまさにcocartesian familyおよびcocartesian functorからなることを示す。
• Structure Homomorphism Principle (SHP): この構築は、構造同一性原理（structure identity principle）の有向版の新しい例を可能にする。著者らは、$\text{Cat}$ を型理論的な連結辞書およびモダリティと組み合わせることにより、モノイダルカテゴリーやmarked categoryのような複雑なカテゴリーを構築する方法を示す。

意義と主張
本論文は、Simplicial Type Theoryの基礎における主要なギャップを埋めることを主張している。$\text{Cat}$ を構築することで、著者らは以下を可能にする：

1. 高次カテゴリー論の内在化: 以前は外部のモデル圏論的な議論を必要としていた主要な基礎的結果を、合成的に型理論内で証明できるようになる。
2. 有向型理論のセマンティクス: $\text{Cat}$ の存在により、「完全に有向な（fully directed）」型理論をSTTへと合成的に翻訳することが可能となり、$\infty$-categoryを適切に捉えるモデルを提供する。
3. 新しい構成: この枠組みは、複雑な代数的構造（例：モノイダルカテゴリー、$E_1$-monoid）の定義や、QuillenのK群の定義を通じた代数的K理論の概念の適用を促進する。

著者らは、彼らのアプローチが（$TT^\triangle$ の公理に依存しており）導出においてモデルに依存しないものである一方で、cubical spacesにおけるモデルによって検証されていることを強調している。彼らは、この研究を高次代数やオペラド理論を合成的に実現するためのステップと見ており、$\text{Cat}$ の構築は完了しているものの、代数的K理論への応用を完全に探求し、理論の計算的な記述を発展させるためにはさらなる作業が必要であると述べている。