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
Mathematics and Computation | How to implement dependent type theory I
How to implement dependent type theory I 08 November 2012 Andrej Bauer Type theory, Programming, Software, Tutorial I am spending a semester at the Institute for Advanced Study where we have a special year on Univalent foundations. We are doing all sorts of things, among others experimenting with type theories. We have got some real experts here who know type theory and Coq inside out, and much mo
Mathematics and Computation | Brazilian type checking
Brazilian type checking 06 May 2014 Andrej Bauer Type theory, Talks I just gave a talk at “Semantics of proofs and certified mathematics”. I spoke about a new proof checker Chris Stone and I are working on. The interesting feature is that it has both kinds of equality, the “paths” and the “strict” ones. It is based on a homotopy type system proposed by Vladimir Voevodsky. The slides contain talk n
What’s the big deal with HoTT? | Existential Type
Now that the Homotopy Type Theory book is out, a lot of people are asking “What’s the big deal?”. The full answer lies within the book itself (or, at any rate, the fullest answer to date), but I am sure that many of us who were involved in its creation will be fielding this question in our own ways to help explain why we are so excited by it. In fact what I think is really fascinating about HoTT
バエズがお薦めするアウディのホット（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
HoTT/Coq 覚書
Homotopy type theory lectures and notes on-line | Existential Type
ホットな話題 - 檜山正幸のキマイラ飼育記 (はてなBlog)
Univalent Foundations at IAS « Existential Type