一度参加した人はその次以降登録しない(けど参加はする)空気が出来上がってるので、このページでは新規参加者だけが表示されるのに留意して下さい。新規参加の方は京都界隈にいるなら飛び入り、リモートなら予めツイッターで @jun0inoue まで Google User ID を DM しておいてください。

前回は Homotopy Type Theory の教科書の9.8節まで読み終わりました。今回は9.9までです。今回で HoTT 本は終わる予定です。次回からは、トピックごとに使用例や解説例を持ち寄るスタイルに変わる予定ですので、各自どういうトピックがよく分かっていないか、どういうトピックの定義や具体例を知りたいか、考えておいて下さい。

http://homotopytypetheory.org/book/

必要な背景知識はどういう資料が選ばれるかによるので一概には言えませんが、とりあえず

• 圏の定義、積対象、和対象、冪対象の定義と具体例いくつか。普遍性という言葉の意味がぼんやりとわかる (≒ Pierce 本 http://www.amazon.com/Category-Computer-Scientists-Foundations-Computing/dp/0262660717 の前半部分ぐらい)
• 詳細はあやふやでもいいし、自分で証明とか導けなくてもいいので、λ算法の表示的意味論ではλ項の意味は⊥を含むCPOから⊥を含むCPOへの連続関数で与える、という話をぼんやりと知っている
• ML や Haskell などでプログラム書ける

ぐらいなら何とかなるんじゃないかと思います。というかならなかったら主催者が泣きます。

第四十三回までのバックナンバーは partake にあります。