Awodey『圏論』第7章その2（7.9から） - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

p.201の真ん中あたりの依存型理論について少々．一つの例をあげると、型INTの整数nに対してそのn次元整数ベクトル（配列）を返す関数vを考えてみる．引数に対応して値域の型が $INT^n$ になっているので、vの型はどうしたもんかということになる．Xを型INTとして、Aの型は余積 $A=\coprod_i A_i$ (ここに $A_i=(INT)^i$ )と考える．するとvの型は $X\to A$ と考えてよさそうである．型理論のCatでのモデル（p.156）を作りたいようなのだが、vの型 $X\to A$ を基本型とするようなモデルであり、かつ元の依存型でない型理論のモデル ${\Large \varepsilon}$ との対応があるようなものを作れないかというのがどうやらここでの動機らしい．その答えは ${\Large \varepsilon} / [ [ X ] ]$ で与えられるのだが、なんでこれなのかとつらつら考えた．任意の型Yに対して、 $[ [ Y ] ] \to [ [ X] ]$ を $[ [ Y ] ]$ の元の全てを $[ [ X] ]$ の0に写像する射を考えると、 $[ [ Y ] ]$ を ${\Large \varepsilon} / [ [ X ] ]$ に埋め込むことができ、かつ、射 $[ [ Y ] ] \to [ [ Z ] ]$ も ${\Large \varepsilon} / [ [ X ] ]$ の射に埋め込むことできる．この対応は関手 ${\Large \varepsilon} \to {\Large \varepsilon} / [ [ X ] ]$ になっていて、また充満かつ忠実である．つまり、 ${\Large \varepsilon} / [ [ X ] ]$ は ${\Large \varepsilon}$ の拡大モデルになっているのである．

　　*****

てつさんの指摘分
http://tetsuro-memo.blogspot.jp/2016/01
でほぼ尽くされていますが、いくつか補足を。

・p.198 真ん中あたり
　誤『 $\beta_{FC}$ の逆像は同型である』
　正『 $\beta_{FC}$ のFでの逆像は同型である』
　原文『the preimage of $\beta_{FC}$ is an isomorphism』

　訳が間違っているわけではありませんが、読んだときちょっとひっかかりました。ちなみにその逆像が同型なのは、 $\beta_{FC}$ が同型だからです.

・p.201 下から11行目
　誤『径数 $x\in X$ に従って』
　正『パラメータ $x\in X$ に従って』
　原文『in a parameter $x\in X$ .』

　『係数』の誤字なのかもしれません.

・p.201 下から8行目
　誤『これらはモデル化でき、対象 $[ [ A ] ] \to [ [ X ] ]$ としてスライス圏 ${\Large \varepsilon} / [ [ X ] ]$ の中、圏 ${\Large \varepsilon}$ の対象としての（閉じた）型Xの上にある．』

　正『これらは対象 $[ [ A ] ] \to [ [ X ] ]$ として、圏 ${\Large \varepsilon}$ の対象として解釈された（閉じた）型Xの上のスライス圏 ${\Large \varepsilon} / [ [ X ] ]$ の中にモデル化できる．』

　原文『These can be modeled as objects $[ [ A ] ] \to [ [ X ] ]$ in the slice category ${\Large \varepsilon} / [ [ X ] ]$ over the interpretation of the (closed) type X as an object of a category ${\Large \varepsilon}$ .』

　誤訳っぽいのでちょっと変えてみました．

・p.203 8行目（てつさん指摘分）
　誤『Uは有限かつ閉と共通部分をとると』
　正『Uは有限であり、(有限の）共通部分の演算で閉じているので』
　原文『since U is finite and closed under intersections,』

　一般にはフィルターは無限積では閉じていないので...細かいことですが...

・p.203 10行目
　誤『しかし、このとき $b_0 < \neg b_0$ かつ $b_0=0$ となる．』
　正『しかし、このとき $b_0 < \neg b_0$ なので $b_0=0$ となる．』
　原文『But then $b_0 < \neg b_0$ and so $b_0=0$ .』