■

[HoTT]HoTTをこっそり学ぶ　その8

　さて、Steve Awodey "TYPE THEORY AND HOMOTOPY"の勝手に翻訳シリーズもいよいよ佳境である。2.3節ははっきり言って急に難しくなっている。今までは何だったんだ。まずは2.3節の前半。


2.3. Homotopical models of type theory
　ホモトピー理論では亜群とその間の準同型は位相空間とその間の連続写像のホモトピー類のモデル(すなわち表現)として現れる。他のモデルとしては単体的集合（simplicial set）がある。Quillenのモデル構造([Qui67, Bou77]参照)のアイデアはそのような異なったホモトピーのモデルの共通の特徴を公理化するというものであり、抽象的で一般的な設定のなかで理論の構築が可能で、個別の設定間の比較もできる。
　この公理論的フレームワークは、亜群、2-亜群、∞-亜群、単体的集合等々あるいは位相空間それ自体といった特定な選択と結びつけることなく、内包的型理論の意味論を一般的に指定する便利な方法を提供する。これに関連した基本的な結果として、内包的型理論が、どのQuillenのモデル圏[AW09] ([War08]も見よ)の中でもモデル化可能であることがいえる。型を抽象的な"空間"X、項 x:X \vdash a(x):A を連続関数 a:X\to A と解釈するアイデアである。すなわち、閉じた項 a:Aは、Aの点であり、等式型の項 p:Id_A(a,b)は、Aの中の道 p:a\rightsquigarrow b (点の間のホモトピー！）である。高次の等式型の項 \vartheta:Id_{Id_A(a,b)}(p,q) は道p,qの間のホモトピーであり、以下同様に高次の等式型の項は高次のホモトピーである。この解釈では、抽象的な"フィブレーション"を依存型の解釈に使い、等式型を抽象的な"道の空間"と解釈する。この解釈は、亜群やその類似物でのモデルを特殊な場合として復元するものとなっている。

　文献[GG08]において、型理論それ自身が自然なホモトピー構造（すなわち、弱分解系(weak factorization system)）を持っており、理論が健全であるだけでなく、そのような抽象ホモトピー的意味論に関して、論理的に完全であることが示された。解釈の厳密性に関するいくつかの"コヒーレンス"問題がまだ解決されずに残っている（再び[War08]、同じく[BG10を見よ]）一方で、これらの結果を組み合わせると型理論の意味論のホモトピー解釈の実行可能性だけでなく、型理論をQuillenのモデル構造の中での理由付けに使用する可能性も明確に示すことができる。言わば、そのことは内包的型理論を"ホモトピー理論の論理学"とみなせることを示唆している。
　この解釈をもう少し詳細に記述するために、最初に標準的な定義のいくつかを思い起こそう。任意の圏\mathcal{C}において、与えられたf:A\to B, g:C\to Dに対して、fがgに関しての left-lifting property(LLP) を持つことを f\pitchfork gと記述する。それは下図のような任意の可換な四角形に対して、

\begin{matrix} \quad A & \overset{h}{\longrightarrow} & C \quad \\ f \downarrow & \exists j \nearrow & \downarrow g \\ \quad B & \begin{smallmatrix} \Large{\longrightarrow}\\ i\\ \end{smallmatrix} & D\quad \\ \end{matrix}

[訳注：斜め点線矢印が出ないので、適当に変えた。]

対角の写像 j:B\to Cが存在して、j\circ f=h, g\circ j=iとなる。\textsf{M}を\mathcal{C}の射の任意の集まりとしたとき、全ての\textsf{M}の射に対して、LLPを持つ射の集まりを^\pitchfork{\textsf{M}}と表記する。同様に射の集まり \textsf{M}^\pitchforkを定義する。[訳注：これは図はそのままでgがfに関して right-lifting property(RLP)を持つと定義し、 \textsf{M}^\pitchforkはすべての\textsf{M}の射に対して、RLPを持つ射の集まりと定義しているという意味である。]　圏 \mathcal{C}における弱い分解系 (\textsf{L},\textsf{R}) は\mathcal{C}の射の2つの集まり \textsf{L}("left-class")、\textsf{R}("right-class") からなっており、次の性質を満たす。

(1) 任意の射 f:A\to Bは f=p\circ iなる分解を持つ。ここに i\in \textsf{L}かつ p\in \textsf{R}である。

\begin{matrix} A & \overset{i}{\longrightarrow} & C \quad \\ & \small{f}\searrow \quad & \downarrow p \\ & & B\quad \\ \end{matrix}

(2) \textsf{L}=^\pitchfork{\textsf{R}} かつ \textsf{L}^\pitchfork=\textsf{R}

　(閉）モデル圏[Qui67]とは、bicompleteな[訳注:small limitとsmall colimitが存在する]圏 \mathcal{C}であり、部分圏として\textsf{F} (fibrations)、\textsf{C} (cofibrations)、\textsf{W} (weak equivalences)を持ち、次の2つの条件を満たすものである。(1) g\circ f=hを満たす3つの射 f,g,hが与えられたとき、任意の2つの射が弱同値[訳注:ここでの弱同値とは単に射が\textsf{W}に入っていること]なら、3つ目もそうである。(2) (\textsf{C},\textsf{F}\cap \textsf{W})と(\textsf{C}\cap \textsf{W},\textsf{F})はどちらも弱分解系である。モデル圏の射fが自明なcofibrationと呼ばれるのは、それがcofibrationであり、かつ弱同値であるときである[訳注:f\in \textsf{C}\cap \textsf{W}]。双対に、自明なfibrationとは、それがfibrationかつ弱同値であるときである[訳注:f\in \textsf{F}\cap \textsf{W}]。対象Aがfibrantと呼ばれるのは、canonical map A\to 1がfibrationのときである。双対に、Aがcofibrantとは 0\to Aがcofibrationのときである。
　モデル圏としては、次のような例がある：


　(1) 位相空間の圏 Top、fibrationsをSerre fibration、weak equivalencesを弱ホモトピー同値の射の集まり、cofibrationsを自明なfibrationに関するLLPを持つ射の集まりとする。このモデル構造における cofibantな対象は、CW複体のように胞体の接着によって作られた空間のretractである。[訳注:これの確認をしようとしたが、これはこれで簡単ではないようである。参考文献の[Hov99]がかなり詳細。ツンドクリスト入りである]


　(2) 単体集合の圏 SSet、cofibrationsをモノ射(monomorphisms)の集まり、fibrationsをKan fibrationの集まり、weak equivalencesを弱ホモトピー同値の射の集まりとする。このモデル構造における fibrantな対象は、Kan complexである。


　(3) (small)亜群の圏 Gpd、cofibrationsを対象への単射である準同型の集まり、fibratoinsをGrothendieck fibrations、weak equivalencesを圏としての同型射とする。この場合、すべての対象は fibrant かつ cofibrantである。

さらなる例と詳細については [DS95, Hov99] を見よ。

　最後に、任意のモデル圏において、対象Aに対する（非常にたちの良い）パス対象(path object) は、次のような自明なcofibration rに fibration pを続けることによる対角写像 \Delta:A\to A\times Aの分解からなることを思い起こそう([Hov99]を見よ)。

\begin{matrix} A & \overset{r}{\longrightarrow} & A^I \quad \\ & \small{\Delta}\searrow \quad & \downarrow p \\ & & A\times A\quad \\ \end{matrix}

パス対象の典型的な例として、Gpdでは適切な"単位区間" Iによる指数(exponentiation)により与えられる。SSetでは、Kan complexである対象Aがそうである。すなわち前者の例では、G^Iは、亜群Gのすべての射の成す"射の亜群" G^{\to}である。パス対象はいつでも存在するが、ユニークに決まるわけではない。多くの例では、それらは関手性を持つように選ばれる。