■

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

　2.3節の後半。実際のところモデル圏であることの確認はかなり難しいようであるが、それをいったん認めて、本題である内包的型理論のモデルへと話を進めてみよう。


（2.3. Homotopical models of type theory の続き）

　今や型理論のホモトピー解釈をもっと正確に記述できる。Curry-Howard対応のアイデアがしばしば”型としての命題”と要約できる一方で、ホモトピー解釈の底にあるアイデアは、それに代わって”型としてのファイブレーション”である。古典的なトポロジー、そしてほとんどのモデル圏においては、ファイブレーション p:E\to Xは、パラメータ x\in Xで連続的に変わっていく対象 E_xの族と考えることができる（トポロジカルファイブレーションでの path-lifting propertyは、あるファイバーE_x=p^{-1}(x)から別の E_yへ、パス x yに沿ってどのように動いていくのかを記述している）。この概念は依存型の解釈を与える。具体的には \mathcal{C}をfinitely completeな圏で（少なくとも）弱分解系 (\textsf{L},\textsf{R})を持つとする。興味深い例はモデル圏から生じるので、 \textsf{L}の射は自明なコファイブレーション、 \textsf{R}の射はファイブレーションとしよう。judgement \vdash A:typeを \mathcal{C}の fibrant な対象 Aと解釈する。同様に依存型 x:A \vdash B(x):typeをfibration p:B\to Aと解釈する。このコンテキストでの項 x:A\vdash b(x):B(x)は、 p:B\to Aの断面(section) b:A\to Bつまり p\circ b=1_Aと解釈する。fibrantな対象を型、依存型をファイブレーションと考えると、等式型 Id_A(a,b)の自然な解釈は、型 x,y:A\vdash Id_A(x,y)が "Aにおけるすべてのパスの作るファイブレーション"となるような、Aの中でaからbへのすべてのパスのファイブレーションである。すなわち、それはAのパス対象である。

[訳注：なんだか横のものを縦にしただけで魂がこもってない気がするので、ここで少しTopで考えてみよう。まず、型A:typeはfibrantな対象 Aと定義された。fibrantな対象とは、canonical map A\to 1がfibrationであったが、Topではこのcanonical mapがSerre fibrationであるのは自明なので、すべての対象はfibrantであり、この制限は実は無い。すべての位相空間が型になれるのである。その要素a:AはAの元と考えるのが自然であろう。依存型 x:A \vdash B(x):typeは、fibration p:B\to Aと定義される（矢印が逆向きなのに注意）。その要素は section b:A\to Bである。この描像では各fibreがいろいろな型（＝位相空間）に対応していることになり、fibre bundleのようにfibreがすべて同型というわけではない。なのでfibrationの定義を少し一般的な Serre fibrationとしているのである。non-dependent type A\to Bは、（普通の意味で）trivialなfibration A\times B\to Aに対応している。さて、等式型 Id_A(a,b)を考察するに、これを適切な位相を入れたパスの空間 P_A(a,b)と同定しておこう。一方、x,y:A\vdash Id_A(x,y)を依存型であると考えれば、何かあるfibration p:X\to A\times Aで、p^{-1}(a,b)\simeq P_A(a,b)となっているものを想定することになる。実際、X=A^I=Hom_{Top}(I,A)とし、pをパスの始点と終点を与える写像とすればよい。定値写像 i:A\to A^Iはホモトピー同値写像であり、対角写像\Delta:A\to A\times Aを\Delta=p\circ iと分解している。A^Iがパス対象であることを示すには、
　1) pがSerre fibrationである
　2) iがcofibrationである（すべての自明なfibration=\textsf{F}\cap \textsf{W}に関するLLPを持つ）
を証明する必要がある。1)について、任意の位相空間Bからのホモトピー写像 h:B\times I\to A\times Aとs:B\times \{0\}\to A^Iで h|B\times \{0\}=p\circ sなるものが与えられたとする。このとき s(b,0)\in A^Iは端点 h(b,0)=(c(b,0),c(b,1))を持つ Aの中のパスの族c(b,t)である。一方、b\in Bを固定すると、h(b,t)=(c_0(b,t),c_1(b,t))は、それぞれAの中のパスであり、c_0(b,t)からc_0(b,\_)を逆に進んで、c_0(b,0)=c(b,0)に戻り、さらにc(b,\_)に沿って c(b,1)=c_1(b,0)へ進み、さらにc_1(b,\_)に沿って c_1(b,t)に連結するパスを作れば、hをA^Iへの持ち上げる写像が作れたことになる。つまり、pはHurewicz fibrationであることがわかり、当然 Serre fibrationである。2)は難しそうな気がする。]

定理2.1([AW09])
　\mathcal{C}をfinitely completeな圏で弱分解系を持つものとし、かつ関手的に安定(stable)パス対象A^Iが決まっているとする。安定パス対象とは、任意のfibration A\to Xと任意の写像 f:Y\to Xが与えらえたとき、evident comparison map f^*(A^I)\simeq f^*(A)^I が同相写像となるものである。
このとき、\mathcal{C}は等式型をもつMartin-L\rm\scriptsize{\ddot{o}}f型理論のモデルとなる。
[訳注:この安定パス対象の条件は、たとえばある項の変数にpropositinaly equalな２項を代入したもの同士がpropositinaly equalになるという、論理としては自然な条件に相当する。たぶん]

　証明では型理論とこの設定における公理的推論の関係性を示すことになる：等式型の規則を検証しよう（補遺をみよ）。fibrantな対象 Aが与えられたとして、judgement x,y:A\vdash Id_A(x,y) は、パス対象のfibration p:A^I\to A\times Aと解釈される。

\begin{matrix} A & \overset{r}{\longrightarrow} & A^I \quad \\ & \small{\Delta}\searrow \quad & \downarrow p \\ & & A\times A\quad \\ \end{matrix}
[訳注:図を再掲]
pがfibrationであるから、構成規則
x,y:A\vdash Id_A(x,y):type
は満たされる。同様に導入規則
x:A\vdash r(x):Id_A(x,x)
も正しいのは r:A\to A^Iが\Delta:A\to A\times A上のsectionとなっているからである。除去と変換の規則については、次の前提が与えられたとしよう。

x:A,y:A,z:Id_A(x,y)\vdash D(x,y,z):type,
x:A\vdash d(x):D(x,x,r(x)).

それゆえ、fibration q:D\to A^Iと共に写像 d:A\to Dで q\circ d=rなるものがあることになる。このデータは次の可換な四角形（外側）を作る。

\begin{matrix} \quad A & \overset{d}{\longrightarrow} & D \quad \\ r \downarrow & \exists j \nearrow & \downarrow q \\ \quad A^I & \begin{smallmatrix} \Large{\longrightarrow}\\ 1\\ \end{smallmatrix} & A^I\quad \\ \end{matrix}

[訳注：再びTopで考えてみよう。Aは位相空間であり、x,yはその元である。型 \textsf{Id}_A(x,y)は、fibration A^I\to A\times Aの、(x,y)上のfibre p^{-1}(x,y)=P_A(x,y)で、zはその元である。 (x,y,z)\in A^I と考えられる。A^Iは位相空間なので型とは言えるが、ただの型であって依存型 A^I\to A\times Aとは異なる。どうやらcontextが位相空間になるということのようである。さて、そうなると依存型Dは、fibration q:D\to A^Iに対応する。また、依存型D(x,x,r(x))は、r:A\to A^Iをr(x)=(x,x,r(x))としたときのfibration DのA上の引き戻しである。dはこのfibrationのsectionを与えているので、引き戻し元のDへの写像と考えて d:A\to Dとしている。この構成から q\circ d=rが成立している。]

qは fibrationであり、rは定義より自明なcofibrationであったから、対角の射であるjがユニークに存在し、項:

x,y:A,z:\textsf{Id}_A(x,y)\vdash \textsf{J}(d,x,y,z):D(x,y,z)
の解釈となる。[訳注:\textsf{J}はqのsectionを与えているのでこの解釈が成立する。]
下の三角形の可換性から、まさに除去規則が出てくる。また、上の三角形の可換性は望まれていたように変換規則となる：
x:A\vdash \textsf{J}(d,x,x,r(x))=d(x):D(x,x,r(x)).
[訳注:ここの＝は無論、Judgemental equalである。]
　この定理の仮定を満たす圏の例としては、亜群、単体的集合、そして数々の単体的モデル圏（例えば単体的層や単体的前層を含む）[Qui67]がある。\textsf{J}項の解釈に対応する対角を埋めるjを”コヒーレントに”選べるのかという疑問がある（たとえば変数の入れ替えに対応する場合など）。この問題に対するいくつかの解答は[AW09,War08,Gar07]で議論されている。ひとつのきちんとした解は、”代数的”Quillenモデル構造に関するRiehl[Rie10]の中で示唆されている。ホモトピー理論から導かれたいくつかのコヒーレントモデルの例に沿ったコヒーレンス問題に関する組織的な調査はvan den BergとGarnerの最近の研究[BG10]に見つけることができる。[訳注:コヒーレント問題とは、圏の中にある種の代数構造を想定したときに結合則などの自然な規則に対応する同型射が存在するがそれらを整合的（コヒーレント）に選んで、定義域と値域が同じなら射として同一になるようにできるかという問題である。例えば結合則を順に行っていく２つの変形 ( (ab)c)d\simeq (ab)(cd)、( (ab)c)d\simeq (a(bc))d\simeq a( (bc)d)\simeq a(b(cd))\simeq (ab)(cd)における同型射(の合成)が最終的に同じ射を与えるべしという非常に強い条件である。]