■

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

　さて、Steve Awodey "TYPE THEORY AND HOMOTOPY"の勝手に翻訳の続きである。もちろん翻訳そのものが目的ではなく中身の解読がメインである。今回は第2章 The homotopy interpretationの2.2節まで、いろいろ調べ物をしながら進めていく。

2.THE HOMOTOPY INTERPRETATION

2.1 Background
　外延的型理論の最近の取り扱いで、最も完全なものはMoerdijkとPalmgrenによる2000年から2002の２つの論文[MP00, MP02]である。また、著者たちは三番目の論文に内包的理論を充てるとしていたが、それは出版されることはなかった[訳注：2020年現時点でも関連する論文はpublishされていないようである。以下に紹介される結果が先に出たためであろう]。恐らく彼らは高階圏論とQuillenのmodel structureを使うつもりであったろう。予備的な結果も述べられることもなかったが、[Pal03]を見よ。
　2006年、Vladimir Voevodskyはスタンフォード大学で“Homotopy lambda-calculus”と題された一連の講義を行った。その中で、simplicial setにおける内包的型理論の解釈が提案された([Voe06]を見よ)。その同じ時期に、独立に、著者（Awodey）と博士課程の学生であったMichael Warrenは、Moerdijkの示唆により、Quillenのmodel structureにおける内包的型理論の解釈を発表した[訳注：2008年にAwodeyとの共著で" Homotopy theoretic models of identity types"がpublishされている。Warrenの関連する学位論文も2008年。どちらもwebで入手可能]。
　これらのアプローチはすべて、Hoffmann と Streicher [HS98]による先駆的研究によるものであり、それをここで要約する。

2.2 Groupoid semantics
型理論のモデルが外延的であるのは、次のreflection ruleが満たされる場合である：

つまり、外延的モデルでは等式型は、項と項が定義的に等しいか等しくないかということ以上の情報を担っていない。内包的理論では型チェックは決定可能(decidable)であったが、等式型を統合するId-reflection 規則を加えた外延的理論ではこれは成立しなくなってしまう。この事実が外延的型理論より内包的型理論が研究される主な動機となっている（内包的理論と外延的理論との違いに関する議論は[Str91]参考のこと）。外延的理論のモデルに対するよい理解は、依存型が局所デカルト閉圏の中で自然な方法で解釈できるということを示したSeely[See84]による。(後のHofmannによる改良[Hof97]の契機となったコヒーレンスの条件の問題があるのだが、ここではそれに関わる必要はない。）[訳注：コヒーレンスの条件とは、局所デカルト閉圏の中で、依存型をpull backとして解釈する際にそれがup to isomorphismにしか決まらなことから生じる問題に関連している。調べているとCurien, Garner,Hofmann『Revisiting the categorical interpretation of dependent type theory』というよさげな文献を見つけた。その文献の導入部でモデルの精密化の二番目としてあげられているのが、ここでいうHofmannの改良である。私は外延的型理論のモデルにそこまで興味があるわけではないのでここはツンドクだが、内包的型理論のモデルでも同様の問題があるのかないのかそこはちょっと気を付けておきたい。]　もちろん内包的型理論もこの方法で解釈できるのだが、その場合は等式型に関する解釈は必然的に上記のような意味で自明なものとなっている。
　内包的型理論の最初の自然で自明でない意味論は、亜群を使ったHofmannとStreicher[HS98]によるものである。亜群とはすべての射が同型射となっている圏である。亜群の圏は局所デカルト閉でなく[Pal03]、そしてモデルは、依存型をモデル化するためにあるファイブレーション（つまりは亜群に値をとる関手）を使用している。直観的な説明としては、亜群上の等式型はの射のなす亜群と解釈され、証明はの中の射となる。この解釈ではもはや外延的な解釈はできない。なぜなら恒等射でない射を持つ異なる要素,の存在がありうるからである。もちろん、多くの異なるそのような射がありえる。しかしながら、型理論とは異なり、高次の等式型に対応するものは存在していない。なぜなら（普通の）亜群は一般的にはそのような高次構造は持っていないからである。ゆえに亜群による意味論では、外延理論からひとつ次元が上がったような形で、全ての高次の等式型が自明となるようなある種の切り詰められた原則を保証することになる。特に、このモデルでは等式型に対する亜群の規則は、命題的等式の成立という形ではなく厳密に満たされている。[訳注：これはが高々１つしかないthin categoryという状況]
　この状況は高次の等式型が非自明であるようにするには、ホモトピー理論の形式化と同じような亜群の高階な類似物の使用を示唆している。そのような高階亜群は（上で議論したように）位相空間の（高次）基本亜群のように自然に表れる。この方向への一歩は、2-亜群の中で内包型型理論をモデル化するのに2次のファイブレーションを使ったGarner[Garar]により踏み出された。種々の打ち切りの公理(truncation axioms)を追加したとき、できた理論はこの意味論に対して、健全かつ完全(sound and complete)である。Warrenは学位論文[War08]の中で、∞-亜群がそのような追加された打ち切りの公理が不要となるようなモデルとなることを示した([War10]も見よ)。しかし、そのようなモデルは型理論としては証明できない合成の結合性といった厳密性条件(strictness condition)を満たしてしまう。これにより完全な内包的型理論の忠実なモデルには、究極的には弱∞-亜群を使う必要があるのが明らかとなった（以下の2.4節を見よ）。