Thierry Coquandが、cubical interpreterでHigher Inductive Typeが使えるようになったとアナウンスしていた。理論的な面で進歩があったわけではないようだけど、cubical interpreterの実装が少し進歩したらしい。 https://github.com/mortberg/cubicaltt 基…

絵が多いので、こっち↓の方に書いた。xyjaxを使いたかっただけというわけではない http://formalgroup.tumblr.com/post/96778113120/simplicial-model-of-type-theory cubical modelのことを書こうと思ったけど、数学の世界では、simplicial setの方が、cubi…

はじめてのCubical http://d.hatena.ne.jp/m-a-o/20131227#p1 の続き。何分できたばっかの処理系なので、上で書いたコードは微妙に動かなくなってしまっているっぽいけど、まぁ少し修正するだけ 実用的には、quotient typeが作れるのは重要な気もするので、…

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 …

その2。 ホモトピー群とEckmann-Hilton argument 型がweak ∞-groupoidだということが分かったので、weak ∞-groupoidに対して、ホモトピー群というものを定義する。type theory的には、ホモトピー群を定義する動機はあまりないけど、数学にinspireされて、(意…

The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思う…

(追記)結局、ここに書いたことは嘘でした( homotopy type theoryで、circleの定義は、higher inductive typeを使って (* this is invalid in Coq *) Inductive circle : Type := | base : circle | loop : paths base base.と書ける(ということになっている)…