帰納じゃなくて昨日は圏論勉強会でした

こっち時間で午前2:30あたりから雪崩式に参加、5時前に眠くなって脱落。
どうも、日本現地会場はエアコンが効かず、大変だったみたいで、途中でファミレスに移動したらしい。お疲れ様でした。

The previous diagram should suggest in which sense b^a “represents” C[a,b]. The eval morphism generalizes the set-theoretic evaluation function eval(f,x) = f(x). Moreover, take c = t, the terminal object. Then as sets. This is particularly significant if C has enough points (why?).

2.3節での、 Cartesian category から Cartesian closed category を導入する直前部分より引用。

どうもこのテキスト（の、少なくとも2章）は、「スノーグローブを計算機で表現する」という裏テーマがあるらしい。参考：

• http://d.hatena.ne.jp/bonotake/20070311/1173577541
• http://d.hatena.ne.jp/m-hiyama/20070226/1172451671
• http://golem.ph.utexas.edu/category/2007/03/snowglobe_models.html

圏論の基礎でも、閉圏の定義と絡めて豊穣圏を導入していることを再発見（第VII章7）*1。多分、上記引用最後の"why?"にも、これのもっとプリミティブなレベルでの考察を筆者は欲しているんじゃないかなと想像。

筆者はこの後、領域理論とかその辺を語りたいのかなぁと想像してたら案の定、この後の"2.4 Examples of CCC’s"は Scott domain と coherent domain の話になってた。

この裏テーマに関する部分はテキストのそこかしこに現れまして、もっと踏み込んだ事を書いてるとこもあって。ただ、その辺をきっちり追いかけるには、ゲーデルエンコーディングや帰納的関数論（特に後者）に関するちゃんとした理解が必要っぽい。なので、これ関連の話題だけ、難易度が異様に高い印象。
（筆者は、そこいらへんの知識は前提としているのか、「そんなん知らなくてもわかるだろ？」と思っているのか(^^;、特に導入などせずにさらっと流してしまっています。）

*1:つか、前々回の疑問だった閉圏の定義、ここにちゃんと書いてるし。