■ - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

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

いろいろぐぐっているうちに次のAwodey氏のレビューペーパーを見つけた。

Steve Awodey "TYPE THEORY AND HOMOTOPY" 2010

これもarXiv.orgで無料で手に入る。こんないいのがあるなら早く教えてよって感じである。全部20ページほどである。今回は一章をさくっと私訳してみよう。文献表は原文を見てほしい。

"TYPE THEORY AND HOMOTOPY"

Steve Awodey

1.INTRODUCTION
　このインフォーマルなサーベイ論文の目的は、幾何学、代数学、そして論理学の間の新しい驚くべき結びつきを紹介することである。それは最近になって知られるようになったPer Martin-L $\rm\scriptsize{\ddot{o}}$ fの構成的型理論のホモトピー理論における解釈の形式であり、その結果としてトポロジー理論の中のある重要な代数構造の新しい例が作られるのである。この結びつきはつい最近に発見されたものであり、今やそのいろいろな側面が多くの研究者により活発に研究されている。（{AW09,AHW09,War08,BG09,GG08,Garar,GvdB08,Lum09,BG10,Voe06]を見よ）

1.1. Type theory
　Martin-L $\rm\scriptsize{\ddot{o}}$ fの型理論は形式的体系であり、本来は構成的数学の厳密なフレームワークを与えることを意図されたものである[ML75,ML98,ML84]。それは型付きλ計算の拡張で、依存型(dependent types and terms)を許すものである。Curry-Howard 対応により、型(type)を命題(proposition)、項(term)を証明(proof)と解釈することができ、この観点により、この体系は少なくとも二階論理より強く、構成的集合論と解釈できることが知られている[Acz74]。もちろんMartin-L $\rm\scriptsize{\ddot{o}}$ fの型理論は、一般化された再帰的定義(generalized recursive definitions)といった構成的数学の大きな部分の形式化に成功している[NPS90,ML79]。さらにこの理論は表現力の豊かさと望ましい証明論的な性質から高級プログラミング言語の開発のフレームワークとしても広く使われている[NPS90,Str91]。
　理論は単純な型 $A$ , $B$ ,...に加えて、それらの項 $x:A \vdash b(x):B$ , そしてインデックス付きの型の族とみなせる依存型 $x:A \vdash B(x)$ を持っている。型を作る単純な操作である $A \times B$ , $A\to B$ と同様に和 $\sum_{x:A}B(x)$ ,積 $\prod_{x:A}B(x)$ を含む依存型に対する操作がある（詳しくはappendixをみよ）。操作 $A \times B$ , $A\to B$ に対するCurry-Howard 解釈は、もちろん命題の連言と選言であり、依存型 $x:A \vdash B(x)$ は述語(predicate)、それを一般化した $x_1:A_1,\ldots,x_n:A_n \vdash R(x_1,\ldots,x_n)$ は関係(relation)、和 $\sum$ と積 $\prod$ はそれぞれ存在 $\exists$ と全称 $\forall$ 量化子である。
　さて、今や一階論理における等号の形式化に対応する原始的な等式関係により、型理論をさらに拡張することは自然である。特に、同じ型 $A$ の２つの項 $a$ , $b$ に対して、 $a$ と $b$ が等しいという命題の証明を表現する新たな型である等式型(identity type) $Id_A(a,b)$ を構成することができる。つまりこの型の項は $a$ と $b$ が等しいという命題の証明となる。ゆえに我々がここで関心を持っている内包(intensional)版の理論では２つの異なった等式の概念を持つことになる。一つは等式型で表現される命題的等式（propositional equality）であり、２つの項は等式型 $Id_A(a,b)$ が項を持つときに限り、命題的に等しいとされる。これに対し、定義的等式(definitional equality)は項の原始的関係であり、型として表現されず、単純型λ計算や通常の等式理論での等式と同じようにふるまうものである。
　もし、項 $a$ , $b$ が定義的に等しいなら（お互いに自由に置き換えることができるため）それらは命題的にも等しい。しかし、その逆は内包的型理論では一般的には正しくない（等式型の規則はappendixに与えられている）。これに対して外延的（extensional）型理論では、２つの等式の概念は追加的な規則により一致するように強制されている。その帰結として外延的な型理論は本質的に標準的な外延的等式関係をもつ依存型理論となる。しかし、よく知られているようにこの単純化の代償として、強い正規化性(strong normalization)、型チェックや項の一致の決定性といった証明論上の望ましい性質を失ってしまう[Str93, Str91, Hof95a]。
　内包的理論では型 $A$ に対して、自明でない構造を持った等式型 $Id_A(a,b)$ が与えられる。もちろんこの構造はHofmannとStreicher[HS98]により見出されており、よく知られた亜群(groupoid)の法則に類似の関係を満たす(原注：亜群は部分的に定義された合成操作をもつ群に似たものである。正確には亜群はすべての射が逆射を持つような圏として定義できる。従って、群はただ一つのオブジェクトを持つ亜群である。亜群はトポロジーにおいて、起点を選ばないように一般化した基本群として現れる。以下を参照。）具体的には命題的等式で仮定された反射性(reflexivity)により任意の $a:A$ に対して等式の証明 $r(a):Id_A(a,a)$ が作られる。これは $a$ に対する恒等射 $1_a$ の役割をしている。そして、もし $f:Id_A(a,b)$ が等式の証明であるとき、（等式の対称性に対応して） $f$ の逆と考えられる $f^{-1}:Id_A(b,a)$ が存在する。そして $f:Id_A(a,b)$ , $g:Id_A(b,c)$ が等式の証明であれば、（推移律に対応して） $f$ と $g$ の合成と考えられる新しい証明 $g\circ f:Id_A(a,c)$ が存在する。さらには各々の型 $A$ におけるこの構造は通常の亜群の規則を満たすことが示せる。しかしこれは重要なことだが、命題的等式による違いを除いてである。この点については以下でまた戻ることにする。
　型理論の構成的な特徴、計算の扱いやすさ、そして証明論的な明快さは、理論の中では $f:Id_A(a,b)$ と表現される項の間の等式のこの微妙な取り扱いにむしろ負っている。計算が複雑な外延的な等式とは異なり、内包的等式の理論の内部における表現性は重要な計算論的な特徴を保ったまま、強力で表現力豊かな体系を導く。しかし、内包性の代償として、自然で型にはまった意味論解釈を見つけることには長い間困難があった（以前の意味論については [Hof97, Car86, Hof95b, Dyb96]を見よ。）
　ここで示す新しい手法は、Quillenのmodel categoryによるホモトピー理論の公理的扱いと（弱-）高階亜群(weak higher-dimensional groupoid)を含む関連する代数的手法を使い、構成的型理論と代数トポロジーとの橋渡しを構築するものである。これを行うには論理的手法に通常の代数的およびトポロジー的手法と結びつけて、ホモトピー理論に迫るのである。そしてそれはホモトピー理論と高階代数の型理論に可能性のある新しい応用を開くものである。それはまた、計算機による証明支援ソフトであるCoqやAgdaといった型理論に基づくホモトピー理論の計算ツールの導入を可能にする（[TLG06]参照）。

1.2. Homotopy theory
　ホモトピー理論では、位相空間とホモトピーの違いを除いた連続写像に関心がある。２つの連続写像 $f,g:X\to Y$ のホモトピーとは連続写像 $\vartheta:X \times [0,1]\to Y$ で $\vartheta(x,0)=f(x)$ と $\vartheta(x,1)=g(x)$ を満たすものである。そのようなホモトピー $\vartheta$ は、 $f$ から $g$ への連続的変形("continuous deformation")と考えることができる。２つの位相空間がホモトピー同値であるとは、行きと帰りの連続写像があり、その合成がそれぞれの位相空間での恒等写像にホモトピーがあるときである。そのような２つの位相空間は連続変形に伴う違いがあるだけと考えられる。ホモロジーや基本群といった代数的不変量はホモトピー不変であり、ホモトピー同値である空間は同じ不変量を持たなければならない。
　ホモトピーのホモトピーを考えるのは自然なことで、高次ホモトピーと称される。位相空間 $X$ と選ばれた点 $p\in X$ を考え、 $X$ の中で始点と終点を $p$ とするパス(path)をホモトピーの違いを除いて考えると点付き位相空間の基本群 $\pi(X,p)$ を得る。Grothendieckのアイデア[Gro83]に沿えば、現代のホモトピー理論はこの古典的な構成をいくつかの方向に一般化させてたものである。その一つは、起点 $p$ を取り去り、すべての点とすべてのパスのホモトピーからなる基本亜群（fundamental groupoid）である。次の例は、ホモトピックなパスを同一視するのではなくパスの間のホモトピーのそれぞれを新しい高次元のオブジェクトと考える（パスを点の間のホモトピーと考えるのと同じように）。この方法を続けることによって、 $X$ の点の作る構造、 $X$ の中のパスの作る構造、パスの間のホモトピー、ホモトピーの間のより高次のホモトピー、さらにもっと高い次元のホモトピーを得る。これらによって最終的に $X$ のfundamental weak ∞-groupoidと呼ばれる構造 $\pi_{\infty}(X)$ を得る。このような高次の代数的構造は今やホモトピー理論で中心的な役割を果たしている( 例えば[KV91]を見よ)。それは基本群 $\pi(X,p)$ や、 $\pi_{\infty}(X)$ の高次ホモトピーを潰した商代数である基本亜群 $\pi(X)=\pi_1(X)$ よりもさらに多くの空間のホモトピー的情報を捉えている。後の2.4節で議論するように、そのような高次亜群が内包的型理論で自然に表れることが最近示されたのである。
　その他の現代ホモトピー理論の中心的概念は、Quillenのモデル構造であり、それは位相空間の本質的なホモトピー的特徴のいくつかを自動的に捉えるのものであり、異なる数学的設定において”ホモトピーする("do homotpy")”ことを可能とし、その２つの設定が同じホモトピー的情報を担うという事実を示すものである。Quillen[Qui67]はホモトピー理論の抽象的枠組みとして、幅広い数学的設定で適用可能なモデルカテゴリーを導入した。その構造は典型的なトポロジーでの例から導かれた3つのクラスの写像の規定(ファイブレション、弱同値、コファイブレーション)からなる。その結果であるホモトピー理論の公理論的枠組みは、特定の設定に関係なく、古典的なホモトピー理論(基本群、写像のホモトピー、強および弱同値、ホモトピー極限等々)の発展を可能とした。よって例えば,位相空間や単体集合（simplicial set）だけでなく、Voevodskyのスキームのホモトピー理論[MV99]やJoyal [Joy02, Joy]、Lurie [Lur09]の quasicategory にも適用できる。ここでの考察（2.3節）において、Martin-L $\rm\scriptsize{\ddot{o}}$ fの型理論がどんなモデルカテゴリーでも解釈できることを示す。このことは型理論の使用が形式的、組織的にホモトピー理論を検証することを可能にする。

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

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