先日の「ホモトピー・ラムダ計算とホモトピー型理論」という記事で、ヴォエヴォドスキーやアウディがやっている(らしき)ことをちょっと紹介しました。
ヴォエヴォドスキーの以前の覚え書きが今はリンク切れになっているのですが、ブックマークコメントでid:salmonsnareさんに新しいURLを教えていただきました。
- ヴォエヴォドスキーの型理論 http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf
ホモトピー型理論は、マーチンレフ型理論をベースにしているらしいです。ikegamiさんにマーチンレフ型理論の資料を教えていただきました。
- Martin-Loef type theory の本:http://www.cse.chalmers.se/research/group/logic/book/ The whole book (200 pages) in Postscript (1.5 Mb) and in pdf (1 Mb).
- http://157.1.40.181/naid/110003743618 龍田真 チュートリアル 型理論II (生IPアドレスなのがプライベート用みたいでちょっと不安)
[追記]さらにid:salmonsnareさんブックマークコメントより追加情報: A very short note on homotopy λ-calculusの新しいURL http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf 。これ絶対に書き足してますね。僕が読んだときはホントに短かったもの。[/追記]