Homotopy Type Theory(HoTT)覚書
[文献とか]
Thierry Coquandのスライド
http://www.cse.chalmers.se/~coquand/equality.pdf
Mike Shulmanのスライド
http://www.math.ucsd.edu/~mshulman/hottseminar2012/01intro.pdf
あたりを読めば大筋は分かる気がする
現時点で、まとまったレビューや教科書のようなものは存在しないけれども、"HoTT-Coqプロジェクト"のレポジトリがgithubにあるので、Coqが分かる人はそれを読むのがよいと思う
https://github.com/HoTT/HoTT
[定義と動機]
HoTTはMartin-Loef type theory等の"先にあるべき"と思われているtype theoryであるけれども、HoTTの定義は、まだ存在しない。その定義をきちんと確立するのが、まず最優先目標。どういうものになるかという、ある程度の指針はあって、それは(∞,1)-toposのinternal logic(に近いもの)だろうと思われている。そもそも、何で(∞,1)-toposかというのは、Matrin-Loef type theoryがホモトピー論的に理解できるという観察に端を発していると思われる。
internal logic of an (infinity,1)-topos
http://ncatlab.org/nlab/show/internal+logic+of+an+%28infinity,1%29-topos
homotopy type theory
http://ncatlab.org/nlab/show/homotopy+type+theory
それで、HoTTが完成すると、何が出来るかというと"functional extensionalityが成立してquotient typeを持つ、まともなtype theory"が出来るかもしれないと期待されている。"まともな"というのは、決定可能なtype checkやclosed termがcanonical formに簡約できる等、"computational"によい性質を持つということを期待している
#実際のところ、homotopy type theoryが"正しい"答えだと考える積極的な根拠は、今のところあんまりないと思う
この問題意識自体は古いものだと思うけど、こういうtype theoryができれば、集合論に代わる数学の基礎となりえる(し、それは基礎として集合論より優れたものになるだろうというのが、Voevodskyのunivalent foundation of mathematicsの目標だと思う)。最近では逆に、homotopy theoryをinternalにどの程度記述できるかという問題意識もある。
quotient typesにしろ、functional extensionalityにしろ、基本的には、等しいということをどう定義すればいいかという問題で、Coq等では、所謂Leibnitz equalityが採用されている。これは自然な等号の定義である一方、CoqやAgdaを使えば分かるとおり、型を同値関係で割るという操作が定義できない。この不都合を回避するために、CoqやAgdaではSetoidを使うというのが、標準的なやり方として採用されている。
A biased history of equality in type theory
http://www.cs.ut.ee/~varmo/tday-andu/chapman-slides.pdf
[歴史]
1995年頃。Hofmann-Streicherの
The groupoid interpretation of type theory
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.606
という仕事が最初の重要な観察。目的は、Intensional Type Theoryのあるモデルを作ることにあり、重要なアイデアは大雑把にいって「x=yであることの証明を、xからyへの射と見れば、groupoidになるよね」という話で、より強くweak ∞-groupoidになるべきことが示唆されている。
homotopy type theory(HoTT)が本格的に始まったのは2006年頃。現在重要な概念は、以下のようなものだと思う
(1)simplicial setsによるtype theoryのモデル化(Streicher,Voevodsky)
(2)univalence axiom(Voevodsky)
(3)homotopy level(Voevodsky?)
(4)path objectsによるidentity typesのモデル化(arXiv:0709.0248,arXiv:0803.4349)
(5)higher inductive types(P.L.Lumsdaine)
Hofmann-Streicherの段階で、weak ∞-groupoidが必要だと分かっていたので、(1)に到達したのは自然な流れ。
Voevodskyは、同時にunivalence axiomを着想して提案している。univalenceは、HoTTの基本的な要請と見られているらしい。univalenceは現在、圏論的な性質としても理解できるようになっている。univalenceを仮定すると、functional extensionalityが従うことが示されている(そして当然canonicityを破るが、type checkがundecidableになるかどうかは不明)
(4)について。(1)に到達すれば、model categoryや(∞,1)-toposを考えるのも自然な流れといえる
higher inductive typeは、homotopy theory in type theoryを展開しようと思えば、必然的に必要となる。例えば、これによって、円周を
(* this is invalid in Coq *) Inductive circle : Type := | base : circle | loop : paths base base.
のように定義できると期待される。これはCoqっぽい記法を使ってはいるけれども、今のCoqでは使えない。baseは円周の"基点"であって、circle型に属する要素と思えるが、loopは、基点から基点へのpathで、これ自体はcircle型に属する要素ではない。circleを単なるclassやstructureではなく、inductive typeと見なすということは、baseとloopで"自由生成される"ような、何らかの普遍的な対象を考えるということ(普通のinductive typeが始代数として捉えられるように)。どういう意味で、"普遍的"なのか、圏論的にきちんと捉えることはできてないと思われる(そもそも、higher inductive typeの定義自体曖昧であるので)
"inductive" typeと呼ぶからには、適切なinduction principle(eliminator)も自動的に従わねばならない。こうしたことは、現在のCoqやAgdaでは無理なので、baseやloopやeliminatorは全てAxiomとして手で入れている(これは注意深くやらないと矛盾を引き起こす可能性があるという意味で危険なので、自動化されることが勿論望ましい)。
通常のinductive typeである自然数natをInductiveを使わずに定義しようと思ったら、以下のような感じになる
Axiom nat : Type.
Axiom O:nat.
Axiom S:nat->nat.
Axiom nat_rect : forall {P:nat->Type},P O -> (forall n:nat,P n->P (S n)) ->forall n:nat,P n.
Axiom compute_O :
forall {P:nat->Type} (f:P O) (f0:forall n:nat,P n->P (S n)),
@nat_rect P f f0 O = f.
Axiom compute_S :
forall {P:nat->Type} (f:P O) (f0:forall n:nat,P n->P (S n)) (n0:nat),
@nat_rect P f f0 (S n0)=f0 n0 (@nat_rect P f f0 n0).circleの場合にどうするかというのは、冒頭のHoTT-Coqレポジトリ等を参照
"まともな"higher inductive typeが定義できれば、functional extensionalityが従うと思われる
http://homotopytypetheory.org/2011/04/04/an-interval-type-implies-function-extensionality/
また、"quotient type"も定義可能になると思われる
http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html
higher inductive typeによって、具体的な空間をcell complexとして表現することができるようになったので、色々な計算ができるようになる可能性もある。
univalenceを仮定すると、円周の基本群がZであることが証明できることは以下で説明されている(Coqによる記述は、HoTT-Coqレポジトリに存在する)
A formal proof that $\pi_1(S^1)=Z$
http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/
#なので、"dependent type theory with univalence"は、単なる(∞,1)-toposよりも強い制約であると思う。
[univalent propertyの圏論的定式化]
univalence axiom in categorical semantics
http://ncatlab.org/nlab/show/univalence+axiom#InCategoricalSemantics
univalent axiom as a property of a model category?
http://mathoverflow.net/questions/73086/univalent-axiom-as-a-property-of-a-model-category
shorter proof of the fact that a universal Kan fibration is univalent
http://www.pitt.edu/~krk56/fiber_bundles_univalence.pdf
[cohesive (∞,1)-topos]
cohesive (∞,1)-toposは、Chern-Weil theoryなど微分幾何を展開できる空間の集まりと思うことが出来る
cohesive (infinity,1)-topos
http://ncatlab.org/nlab/show/cohesive+%28infinity,1%29-topos
cohesive (infinity,1)-topos -- structures
http://nlab.mathforge.org/nlab/show/cohesive+%28infinity%2C1%29-topos%20--%20structures
cohesive (infinity,1)-topos -- structures II
http://ncatlab.org/nlab/show/cohesive+%28infinity,1%29-topos+--+structures+II
cohesive (∞,1)-toposとそれに関わる概念をHoTTで記述するというのは、
HoTT Cohesion ? Exercise I
http://golem.ph.utexas.edu/category/2011/11/hott_cohesion_exercise_i.html
HoTT Cohesion ? Exercise II
http://golem.ph.utexas.edu/category/2011/11/hott_cohesion_exercise_ii.html
Mike Shulmanのgithubレポジトリ
https://github.com/mikeshulman/HoTT/tree/master/Coq/Subcategories
cohesive homotopy type theory
http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory
あたりで議論されている
