■

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

今回はHoTT Bookにもどってみる。このテキストは"HoTT Book"でぐぐれば公式でPDFを無料でゲットできる。さて、まだ１章のFoundationを少しずつ読み進めている段階であるが、Introductionを読み返してみるとちょっとわかった部分があったので備忘録として書いておきたい。無論、今の理解の及ぶ範囲なので間違いもあるかもしれないのでそこはご容赦を。

Homotopy type theory
を" is a point of the space "と解釈するのがHoTTの発想である。ただ、そうなるとtype とは何ぞや、どうやって位相空間（もどき）をtypeとして実現するのかという点が疑問となる。ただ、どうやらここでの話は前回紹介したidentity type をHomotopy equivalenceと解釈するモデルの話のようで、文献の一つとして

Awodey and Warren."Homotopy theoretic models of identity types.",Mathematical Proceedings of the Cambridge Philosophical Society, 146:45-55, 2009
（これもぐぐれば arxiv.orgから無料で入手できる。いい時代になったものである。）

があげられている。これも論文つんどくリストにいれておこう。

spaceとしてのtype の構成に関してはどうやら Higher induction typesの話のように思われる。ただ、ここでの説明はなんだかイメージっぽい話で数学ではないし、文献もあがっていない。ぐぐってみると唐突にCoqでの実装の話になってみたり、非常にアヤシイ感じがする。HoTT本の６章がそれにあたっているが、ちらっと覗いてみてもなんじゃらほいな印象。 Quillen のmodel categories と関連がある部分と想像しているが、今のところは保留。

Univalent foundations
最初読んだときはまったく理解不能であったが、今ならすこしは理解できそうである。
universe のelementとしてtype をと表記する。あたかもtypeとそのelementの関係のような表記であるが、実際にそのように、つまりをtypeとして解釈するのである。もちろん前回紹介したようにそのままだと理論が矛盾してしまうので、はある階層のuniverse のことであり、添え字を省略していると理解しなくてはならない。さてその時にidentity type を考えてみよう。今度はtype間の同一性を問題にしているわけである。ところが話がややこしいのは、もうひとつまったく別の基準から２つのtype , がequivalentであることを表現している type が与えられているとしているのである。これがあんまり具体的に述べられていないのでなんだかよくわからないわけであるが、実はHoTT本の2.4節にその記述がある。そこでの構成でははtype , がHomotopy equivalentであるというような意味を持っているとのことである（今は深入りはすまい）。さて、テキストではをと書いているが、ももtypeなので、

というtype が作れる。identity が成立すればEquivも成立するのでこのtypeはelementを持っているが、Univalent Axiomはこの逆も成立するという公理である。ただ、Introductionでコメントされているように、あるobjectがequvalentだったら実はidenticalであるという意味なので構造がスカスカ（skeletal）である。テキストではこれは逆にidentityが拡張されているのだと述べているが、なんだかなぁである。この同値類を同一視して扱うような発想は以前にもこのブログでアブナイ思想と述べたことがあるが、それは２つのobjectが同値かどうかの判定を行うアルゴリズムが存在しない場合があるためである。HoTTはどうであろうか？ この逆とは、proof が与えられたとき、proof が構成できるという意味であり、そもそもproof が構成できる時点でアルゴリズムの存在は大丈夫そうである。ただ、が任意の,に対して構成的に判定できるアルゴリズムがあるというのはかなり強い制限である。これは結局とかの構成がどうなっているかに依っているのであり、ここは注意が必要と個人的には思っている。