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も真にする』という意味である. はどんな解釈でも真にならない命題、はどんな解釈でも真になる命題の意味で…