UbuntuへのAgda2.4.2インストールで詰まっている話

Agda

Ubuntu（正確にはXubuntu14.02）にAgda2.4.2をインストールしようとして（cabal install agda）、なんかHaskellのあたりでうまくいかなくて困った。が、
http://stackoverflow.com/questions/25104367/ghc-incompatibility-installing-haskell-src-exts-via-cabal
にまったく同じ問題と思われるものが転がっていたので、これをあとで試してみる。

A new approach to the semantics of model diagrams

論文

http://drops.dagstuhl.de/opus/volltexte/2013/3898/pdf/4.pdf
http://static.googleusercontent.com/media/research.google.com/ja//pubs/archive/40678.pdf
結局ワールドというのはモデル図にもなるという話なのか、なんかすごいな。あとでちゃんと読むが、��typeという単純な構造がいろいろなものに適用できるというのは面白い。

Agda

とりあえず、LuaLaTeX上でLuaTeX-jaパッケージを動かして、日本語表示とunicodeのマニアックな記号表示を両立されるところまではできたぞ。環境はWindows7上のTeXWorks。

フォントの制御はまだうまくできていないが、unicodeの記号および日本語はPDFで表示できるようになった。とりあえず一段落。

unicode部分のフォント指定。いまは日本語フォント（上記PDFではMSゴシック）になっているようだが・・・
- http://ctan.math.washington.edu/tex-archive/macros/latex/contrib/fontspec/fontspec.pdf あたりをきちんと読む必要がある。
- 気持ちとしては、Emacsのようにこのコードからこのコードまではこのフォント、とできたらいいのだが。それか、書いてあるところにいちいち直接フォント名指定、ということなのかな。

Agda

今日から1日3コマ×3週間でAgdaを使った定理証明実習という講義がはじまる。ぼくはTAとして参加予定で現在インストール手順など作っています。思ったこと。

研究に付随する趣味兼実用の世界やな・・・論文になるわけではないが、重要な仕事。

とりあえず、学生の反応を観察して、なんのこっちゃようわからんのは何故か？というところは明らかにしていきたい。

お久しぶりです。大学の近くに引っ越して、段ボールの山と格闘しつつ研究を始めています。

とりあえずAgda含む日本語論文を書く環境を何とかしようと思い、LuaTeX-jaをごにょごにょしようと思っていたのですが、冷静に考えてみるとTeXの何がどう動いているのかさっぱり理解できていないことに気付いたので、久々に

を取り出して読んでました。ようやくフォントのこととか文字のエンコードの話とかが、少しずつわかってきた感じ。まだまだですが。新版を買ったので餞別にこの本くれたOくんありがとう。

http://d.hatena.ne.jp/kiiiino3/20140730/1406751992
でも書いたとおり、ドイツに行かなかった代わりにまとまった読書をしようと思い。

の1章を読んだ。実は自主勉強会ですでに6月ぐらいから読み始めていたのだが、改めて最初のページから読み返した。読み返したら、自分がいかによくわかっていなかったかが、よくわかった。

まあ、合宿というと1日12時間ぐらい読んでたのかという話になるのだが、全然そんなことはなく、1日せいぜい3-4時間ぐらい。数学の勉強というのはそれぐらいが限界だとぼくは思っている。今のところ。

とりあえず、盆休みも1日1時間ぐらいはCategory Theoryに向き合えたらいいなと思う。こどもが起きる前に早起きする、ぐらいしかなさそうではあるが・・・。

あと、自分がいかによくわかっていなかったか、というのには、自分が悪いという気持ちと、本が悪いという気持ちと2つあって、もっと省略せずに本当に隅から隅まで丁寧に解説した圏論の本、というのは欲しい。これは自分で書くしかないな。気持ちとしては、

の圏論版。