■

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

　さて、すでに終盤に突入している。2.4.1節に取り組もう。ホモトピー解釈からさらに進んで、Martin-L\rm\scriptsize{\ddot{o}}f型理論をホモトピー理論の論理学としたいのである。


2.4. Higher algebraic structures

　ホモトピー解釈によって本質的に健全性と完全性が与えられたので、さらにホモトピー理論の言語としての論理システムをどのように表現すればよいのだろうか？ この観点からは内包的理論における位相空間としての型について考えみよう。型 Aの項は”位相空間”Aの点であり、等式型 \textsf{Id}_A(a,b)は aと bを結ぶパスの集まりとして表現され、高次の等式はパスの間のホモトピー、パスのホモトピーの間のホモトピー等々となる。ホモトピー論に関連するどんな事実、性質や構造が論理によって表現可能かどうか問うてみる。パスの集まりやホモトピー写像の集まりが亜群を成さない（ホモトピー同値の差を除けば亜群となる）というトポロジー的事実は、等式型の集まりが命題的等式の差を除けば亜群の公理を満たすという事実をもちろん思い出させる。このホモトピー論と型理論の明白なアナロジーは今やまさに論理のホモトピー解釈によって厳密にでき、もちろん同じ事実として認識が可能となっている。位相空間の基本弱ω亜群は、まさに論理システムの中における構成である。それは言わばこれから説明しようとするホモトピー理論の論理に属している。

2.4.1. Weak ω-groupoids
最近、Peter Lumsdaine [Lum09]、および独立にBenno van den Berg と Richard Garner [BG09, vdB]によって、型理論におけるある固定された型 Aの等式型の塔[訳注:等式型、等式型の等式型、等々]が、弱ω-亜群([KV91, Lei02, Che07, Bro87])と呼ばれるホモトピー理論で生じるものとまったく同じような無限次元の代数的構造を持っていることが示された。
　もう少し詳細に言うと、高階亜群に対する globular approach [Lei04, Bat98]では、弱ω-亜群は対象("0-cells")、対象の間の射（"1-cells"）、1-cellの間の2-cell等々と考察している亜群の種類（strict、弱、n- あるいは ω-等々）に応じて様々な合成操作と法則を持っている。最初はglobular集合の概念が必要であり、それは一つの”無限次元の”グラフと考えられる。具体的には、globular集合（[Bat98, Str00]）とは次のような射によって生成される圏 \mathbb{G}上の前層(presheaf)である。

0\begin{smallmatrix} s_0 \\ \LARGE{\rightrightarrows}\\ t_0 \\ \end{smallmatrix} 1 \begin{smallmatrix} s_1 \\ \LARGE{\rightrightarrows}\\ t_1 \\ \end{smallmatrix} 2 \begin{smallmatrix} \\ \LARGE{\rightrightarrows}\\ \\ \end{smallmatrix} \dots
ただし、ss=ts,st=ttの関係を満たしているものとする。
[訳注：ここでいう圏\mathbb{G}上の前層とは、\mathbb{G}から集合の圏 Setへの反変関手のことである。以下の説明でA_nとはこの反変関手Aでの\mathbb{G}の対象 nの像である。以下の本文の説明を参照]。もっと具体的には、globular集合 A_{\bullet}は、それぞれの n\in \mathbb{N}に対して、”n-cell”の集合 A_nを持ち、それぞれの (n+1)-cell xは平行であるソースとターゲットの n-cell s(x),t(x)を持っている(正の次元をもつ cell x,yが平行であるとはs(x)=s(y)かつt(x)=t(y)のときとする。0-cellはすべて平行であるとする)。[訳注：このことはs(s(x)=s(t(x)),t(s(x))=t(t(y))から従う。同じ記号s,tを使っているが、反変関手であるから\mathbb{G}上の関係式と射の向きが逆になることに注意。s,t:A_{n+1}\to A_{n}と次元は下がる。]

（FIGURE1はちょっと再現が大変なので省略）

例として、型理論\mathbb{T}において型 Aが与えられたとして、型

A,\textsf{Id}_A,\textsf{Id}_{\textsf{Id}_A},\dots,
の項はevident indexing projection、たとえば p:\textsf{Id}_Aに対して s(p)=a, t(p)=b と共に globular集合 \hat{A}を作る。
[訳注：A_0=A,A_1=\{p:\textsf{Id}_A(a,b)| \forall a,b:A\},A_2=\{p:\textsf{Id}_{\textsf{Id}_A(a,b)}(x,y)| \forall a,b:A, \forall x,y:\textsf{Id}_A(a,b) \}等である。例えば、p\in A_2とするとs(p)=x,t(p)=yでs(s(p))=s(t(p))=a,t(s(p))=t(t(p))=bと確かに要求された関係式が成り立っていることがわかる]
　
　strictなω-亜群は無限次元の亜群で、すべての次元で結合則、単位元そして逆元の法則がcellの間の等式で与えられている。そのような亜群は底にあるそれぞれの次元のcellからなる globular集合を持ち、任意のglobular集合 A_{\bullet}は、自由 strict ω-亜群 F(A_{\bullet})を生成する－任意の集合が自由群、任意のグラフが自由亜群を生成するのと同じように。 F(A_{\bullet})のcellは自由な（strictに結合則を満たす）A_{\bullet}のcellの結合とその形式的な双対であり、 F(A_{\bullet})の単位元であるcellからくる退化した結合(degenate pastings)も含んでいる。strictなω-亜群においては、より低い次元の共通の境界に沿ってcellを結合することができる。その結合は種々の結合則、単位元、そして交換法則（interchange laws）を満たしている。それらの法則は、ラベル付けされた結合図式が唯一の合成元を持つという一般化された結合法則で捉えることができる。
[訳注：これだけの説明ではなんのこっちゃである。恐らくA_{\bullet}における元の合成はその元があたかも射であるように思って、tとsで与えられるtargetとsourceとが一致するときのみ合成可能とすることになっているはずである。この合成により自由生成されたものとし、単位元との結合を除いて、何か別の元に変換されるような関係式は無いとした場合が strictなω-亜群であろう。]

　これに対して弱ω-亜群ではstrictな結合則は期待できず、それぞれの結合の図式に対して合成写像を複数得るということがある。しかし、それらの合成写像は次の次元のcellの違いを除いて一致すると要求することにしよう。そして、これら結合的cellはそれ自身のコヒーレンス法則を満たすとし、以下同様である。［訳注：いろいろな可換図式がそれより高次からやってくる射の違いを除いて成立するということ。具体例が欲しいところである。］

　さて、これは内包的型理論での状況と正確に同じである。例えば、等式の推移則の証明（witness）を構成しようとしたとき、単一のcanonicalな候補があるということではない。具体的には、合成の図式：

\cdot \longrightarrow \cdot \longrightarrow \cdot
あるいはもっと具体的に、次のような項 c
x,y,z,:X,p:\textsf{Id}(x,y),q:\textsf{Id}(y,z) \vdash c(q,p):\textsf{Id}(x,z)
として、(Id-ELIM)をpおよびqに適用することで、2つの似たような自然な項 c_lとc_rがそれぞれに対し存在する。これらは定義的に等しいというわけではなく、命題的に等しい。それはつまり 2-cellの差を除いてということであり、次のような項eが存在する。
x,y,z:X,p:\textsf{Id}(x,y),q:\textsf{Id}(y,z) \vdash e(q,p):\textsf{Id}(c_l(q,p),c_r(q,p))

すなわち、次の定理を得たことになる。

Theorem 2.2 ([Lum09,BG09])
Aを内包的Martin-L\rm\scriptsize{\ddot{o}}f型理論\mathbb{T}の任意の型としたとき、

A,\textsf{Id}_A,\textsf{Id}_{\textsf{Id}_A},\dots
といった型の項が成すglobular集合 \hat{A}は弱ω-亜群の構造を持つ。

　さて今やこの特別なω-亜群のどんな特別な性質が型理論の構成に役に立つかと問うことは自然である。関連する他の自由代数の統語的な構成に照らすと、上記のω-亜群が適切な同値関係の概念の下で自由弱ω-亜群であるというのは妥当な推測である。この疑問については以下でまた立ち返る。


[訳注：定理2.2の直前に述べられていることを確認してみよう。Id-ELIMについては本論文のAPPENDIX Aにあり、次のようである。

x:A,y:A,z:\textsf{Id}(x,y)\vdash B(x,y,z):type
\Large\frac{c:\textsf{Id}_A(a,b)\quad \quad x:A\vdash d(x):B(x,x,r(x))}{\textsf{J}(d,a,b,c):B(a,b,c)}
ぱっと見なんのこっちゃだが、型Aの要素であるx,yとz\in \textsf{Id}(x,y)の依存型B(x,y,z)が与えられたとして、x=y,z=r(x)という限定された依存型B(x,x,r(x))に要素d(x)があれば、B(x,y,z)そのものにも要素が存在するという内容である。
さて、まずはB(x,y,z):\equiv \textsf{Id}_A(y,z)\to \textsf{Id}_A(x,z)としてみる。ここでz:Aはパラメータとして固定していると考える。p\in \textsf{Id}(x,y)は含んでいないが、x=yとした\textsf{Id}_A(x,z)\to \textsf{Id}_A(x,z)には恒等写像1_{\textsf{Id}_A(x,z)}が存在しており、Id-ELIMよりc(x,y,z):\textsf{Id}_A(y,z)\to \textsf{Id}_A(x,z)が存在する。ところで仮定q:\textsf{Id}_A(y,z)があるので、c(x,y,z)(q):\textsf{Id}_A(x,z)となり、たぶんこっちがc_rで、同様にB'(x,y,z):\equiv \textsf{Id}_A(x,y)\to \textsf{Id}_A(x,z)から、c'(x,y,z):\textsf{Id}_A(x,y)\to \textsf{Id}_A(x,z)を経て、c'(x,y,z)(p):\textsf{Id}_A(x,z)がc_lである。どっちがどっちでもいいのだが。この2つの\textsf{Id}_A(x,z)の要素がpropositionalに等しいことを示すには、等式型\textsf{Id}_{\textsf{Id}_A(x,z)}(c(x,y,z)(q),c'(x,y,z)(p))の要素を構成する必要がある。この要素をId-ELIMを繰り返し適用することで構成してみよう。
\textsf{Id}_{\textsf{Id}_A(x,z)}(c(x,y,z)(q),c'(x,y,z)(p))の要素が欲しければ、y=x,p=r(y)とした\textsf{Id}_{\textsf{Id}_A(y,z)}(c(y,y,z)(q),c'(y,y,z)(r(y)))に要素があればよく、これの要素が欲しければ、z=y,q=r(y)とした\textsf{Id}_{\textsf{Id}_A(y,y)}(c(y,y,y)(r(y)),c'(y,y,y)(r(y)))の要素があればよいが、この最後の型はc,c'の定義に戻ると\textsf{Id}_{\textsf{Id}_A(y,y)}(r(y),r(y))に等しく、r(r(y))を要素として持っている。逆にたどればテキストでいうe(p,q)の存在が示せたことになる。]