3 01 A Functional Programmer's Guide to Homotopy Type Theory
はじめてのCubical -
Thierry Coquandたちが、univalenceと両立する、dependent type theoryの新しいcomputationalなmodelを作ったと言っている A model of type theory in cubical sets http://www.cse.chalmers.se/~coquand/mod1.pdf これを実装した処理系は Implementation of Univalence in Cubical Sets https://github.com/simhu/cubical に置いてある。適当にcabal installとかすればインストールできる #新しい処理系なので、若干の仕様変更により、ここに書いたコードは、そのままでは動かなくなっているっぽい。面倒なので修正はしない 細かいことはわたしもよく分かってないけど、今までHoTT(homot
バエズがお薦めするアウディのホット（HoTT）論文 - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日紹介したバエズの記事には、たくさんのコメントが付いています。現時点（2013-12-05）で48個のコメント。 最初の数個のコメントに目を通してみたら、"Notions of Sameness" に関連する解説として、スティーブ ・アウディの論文が参照されていました。バエズ自身が次のように推奨しています。 If you want to read something more about what I just said, I strongly recommend this: 私（バエズ）がこの記事で書いた内容に興味を持って、もっと資料を読んでみたいなら、この論文がとてもお薦め： Title: Structuralism, Invariance, and Univalence (November 14, 2013) Author: Steve Awodey URL: http://www
Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -
The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする 一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や
The HoTT Book
Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program Institute for Advanced Study Buy a hardcover copy for $21.00. [620 pages, 6″ × 9″ size, hardcover, first-edition-1277-g3274cb3] Buy a paperback copy for $14.00. [620 pages, 6″ × 9″ size, paperback, first-edition-1277-g3274cb3] Download PDF for on-screen viewing. [490+ pages, letter size, in color, with col
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
observational type theory in nLab
Homotopy type theory lectures and notes on-line | Existential Type
ホットな話題 - 檜山正幸のキマイラ飼育記 (はてなBlog)
Univalent Foundations at IAS « Existential Type