では、命題9.16を詳細に見ていく。まず、任意のに対して、関手の自然同型の構成の復習から。自然同型であること示すのには、補題7.11から各々の対象上で同型であることを示せばよいので、となっているかが問題となる。 添え字圏は命題8.10で構成されており、…

さて、本節開始直後に なる随伴の系列が紹介されているが、実際のところV,F,Rについては本書では何も（定義すら）述べられていないようだ。いろいろ調べたところ、その答えはMac Lane本の4章2節の練習問題の中にあった。 :Setsの対象（集合）に対して、その…

前半はあまりコメントするところがないが、p.250の最後の"栞"はなんのこっちゃであって、ここでいう"bookkeeping"とは、全称化の規則で（次の図式はただの推論の図）、"ただしは自由変数記号でには現れないものとする。"というこの”ただし”以下の付帯条件を…

念のため、前順序と半順序の違いは、半順序では、反対称律（ かつ ならば ）が成立している点である。ということは、前順序では順序関係がループになっているケースも許しているわけである。ちなみにテキストの骨格的（skeletal）とは、圏論用語では対象間の…

例9.8の『左随伴は何であろうか？』に答えてみる。 から、問題となる図式はとなるが、下はしか射が無いので、対応する上の射も一つしかない。つまり、がの始対象である。答えは、の始対象となる。その後の『この最後の例は次の一般的な事実の明白な事例であ…

さて、命題9.4である。まず注意として、原文でも似たような書き方なので罪は同じだが、条件2から条件1を言う時に、条件2の中に直接のデータとしてはは与えられておらず、すぐ下のをの定義として、これが自然変換であることを示す必要がある。それゆえp.240終…

ずいぶん放置していたが、リアルのお仕事が結構忙しかったのである。しかし、9章は『本書の見せ場』と著者自ら書いているところなので、こちらも書かずにはおられない。9.1節は随伴の導入という位置づけらしく、次節の定義9.6(p.242)で正式な定義がなされる…

結構早い時期に途中まで記事を書いて放置して、もうとっくにGWも終わってしまった。ゆるゆるにもほどがあるが、いつもはこんなペースである。 さて、ついにトポスの登場である。といってもちょろっと紹介されているだけではある。参考文献にトポスのバイブル…

今回はなかなか手強かったが、ゆるゆると行きたい。 命題8.7について少々コメントを。極限の存在をいきなり仮定して計算するとこうなるので定義はこうする（8.4）とよいというのは発見法的でアリなのだが、そこで証明が終わってしてしまうのでなんだか気持ち…

8.1節の後半は代数的位相幾何学からの例だが、p.211のダイヤグラムはSimplicial Complexの説明である．圏の定義は7章のどこにあったかよくわからないが、8章末の問題4に『は有限順序数とその間の順序を保つ写像』とあるのでこれを採用すればよい．一番目の図…

p.201の真ん中あたりの依存型理論について少々．一つの例をあげると、型INTの整数nに対してそのn次元整数ベクトル（配列）を返す関数vを考えてみる．引数に対応して値域の型がになっているので、vの型はどうしたもんかということになる．Xを型INTとして、Aの…

いきなりCatの余積で詰まった．積の定義はp.47にあるのだが、余積の定義は本書には見あたらないのだ．しかし、考えるとSetsと同じDisjoint Unionでいいようである．さっそくp.168の反例にあたってみる．C+CのオブジェクトはCのオブジェクトを直和成分のどち…

直観主義命題計算と型付きラムダ計算がCurry-Howard対応で同型になるということは計算機の世界ではよく知られているらしいが、命題6.14では直観主義命題計算にはハイティング代数、命題6.17ではラムダ計算にはデカルト閉圏に対して完全性定理が述べられてお…

怒涛のように論理学関連からの例が出てくるが、6.4の随意(entailments) について一言. これはモデル理論の概念で『ある解釈Mがpを真にするならば、qも真にする』という意味である. はどんな解釈でも真にならない命題、はどんな解釈でも真になる命題の意味で…