いつか、Coqで書こうと思う。 weak 2-categoryの定義としては、bicategoryが標準的。bicategoryについては、 Basic Bicategories http://arxiv.org/abs/math/9810017 がよいと思う。bicategoryの定義から、coherence theoremまで10ページほどで書かれてる。 …

Coqのバージョンは8.3 どうでもいい話その1。集合の代わりにSetoidを使うという点について。色々見てると、数学をCoqで形式化する際には、Setoidを使うのが割と普通であるらしい。その正当性は、何によって保証されるのか?とか思うものの、そもそもZFC集合論…

この間、(技術書・専門書の)翻訳が儲からないという話を聞いた。しかしまあ、聞くまでもなく、技術書・専門書なんて、数千部売れる程度というのが相場らしいので、3000円で2000部だと売り上げ600万円、5000円で3000部で1500万円とか、売り上げ数千万円、下手…