HoTT のモデルとそれにつながりそうな文献

先日のメモを詳しくしてみた。ほとんど introduction しか読んでないので正しくないことを書いている可能性もそこそこあります。そういえば 2000 年代前半の文献をあまり見かけないのはなんでだろう。

ここに挙げた文献の参考文献リストとか homotopy type theory in nLab とか References | Homotopy Type Theory とかを見れば，他にも文献はたくさん見つかります。

現状では，types as spaces という見方はだいぶ確立されているというか informal には受け入れられていて，それを数学的に justify しようとしていくつかのアプローチが提案されている，というところなんでしょうか。何のために justification を求めるのかということがよく見えていないんですけど，一つには無矛盾性でしょうか。

Syntax and Semantics of Dependent Types (Hofmann 1997)

依存型の入った型システムとその意味論の解説。HoTT に限らず依存型の圏論的意味論をやる準備として読むとよいかもしれない。ただし圏論をそこそこ知らないと読めない気がする。

The groupoid interpretation of type theory (Hofmann, Streicher 1998)

http://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/
型を groupoid で解釈するという，後の HoTT につながるアイデアの初出。たぶん conference version がもっと前に出ているけど，こちらのほうが読みやすそう。
主な内容は，intensional type theory のモデルで UIP (uniqueness of identity proofs) を満たさないもの，つまり identity type が複数の要素を持つモデルの構成。UIP が導けるのかどうかはこの時点では未解決だったようで，UIP の導出可能性はこれで否定的に解決したという趣旨のことも書いてある。

Homotopy theoretic models of identity types (Awodey, Warren 2007)

http://homotopytypetheory.org/references/awodey-warren-homotopy-theoretic-models-of-identity-types/
ホモトピー論と型理論を関係付けようとする最初の文献だと思う。11 ページと比較的短いけど，その分さらっと書いてある気もするので，Warren の博士論文のほうが詳しくて読みやすいかも。
ホモトピー論に由来する概念であるモデル圏を使って intensional type theory のモデルが作れることを言っている。それからモデル圏の internal language についての言及があって，一般のモデル圏では identity の除去規則 J と代入の可換性（coherence と呼ばれている）が成り立たないため，internal language は Martin-Löf type theory とは異なるということが指摘されている。

Homotopy Theoretic Aspects of Constructive Type Theory (Warren 2008)

http://mawarren.net/papers/phd.pdf
博士論文。大雑把に言えばモデル圏が型理論のモデルになるという内容で，Awodey and Warren 2007 と趣旨は同じだけど，より詳しい説明を含む。細かいことはこちらを見ないと書いてなさそう。Awodey and Warren 2007 でも指摘されている coherence など，細かく見ていくとけっこう微妙なところがあるようで，そのあたりのことが議論されているようだ。それから 1-truncation を満たさないモデルについても ω-groupoid を使って構成していて，これは先行の論文には書いてなさそう。

Topological and simplicial models of identity types (van den Berg, Garner 2011)

http://arxiv.org/abs/1007.4638
この頃には型を空間とみる視点は既に確立されたものとして扱われている様子。ただ先行する Awodey and Warren の論文で指摘されていたように，きちんとモデルを作ろうとすると coherence が成り立つように条件を追加する必要がある。どうもこれが現在までずっと主な困難になっているらしい（2014 年の Awodey の論文でもその点は言及されている）。
この論文ではそのための追加の条件を与え，例として Top と SSet を使った新しいモデルを作っている。アイデアの一つに fibration ではなく cloven fibration を考えるというのがある。*1cloven weak factorization system が適当な条件を満たすと identity type の健全なモデルができる，らしい。この「適当な条件」については，一般にはそれを満たすものが存在するとは限らないが，存在するための十分条件を与えている。Top と SSet はいずれもこの条件を満たすように構造を入れることができるのでモデルが作れる，という流れだと思ったけどあまり自信がない。

The Simplicial Model of Univalent Foundations (Kapulkin, Lumsdaine, Voevodsky 2014)

http://arxiv.org/abs/1211.2851
今 arXiv に上がっているのは version 2 で，version 1 は 2012 年。どこが差分かは確認してない。
この論文は，タイトルにもあるように univalent foundations の研究という色が強い。この記事に挙げた他の論文ではあまり univalence には言及されていないし，そもそも universe を扱っていない場合が多いように思うので，そのあたりが他との方向性の違い。といっても，ここではたまたま他のものを取り上げなかっただけで univalence に関する論文自体はいくつもある。
技術的な内容は，simplicial set を使った univalence axiom を満たすモデルの構成。それから無矛盾性にも言及している（単にモデルの存在の系として出るんだけど）。

Natural models of homotopy type theory (Awodey 2014)

http://arxiv.org/abs/1406.3219
representable natural transformation という概念（知らない）を使った新しいモデルの構成。中身はどういうものか全く確認できてないけど，これ以前の Awodey の論文にある homotopy theoretic model は coherence に関する不自然な条件を入れる必要があった，と導入部で書いているので，それとは別のアプローチか。

*1:雑に言うと fibration の定義はある性質を満たすものが存在するという形になっているが，cloven fibration ではその性質を満たすものが具体的に与えられているという定義になっている。単に存在すると言っているだけ (merely exists) なのと具体的に与えられている (constructively exists) のは違う，という HoTT 本で強調されていた話を連想させるのは面白い（けど関係があるかどうかは知らない）。