読者です 読者をやめる 読者になる 読者になる

北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

CLTT p45 Exercises 1.3.1 (i) の証明の一部

math

CLTT読書会のまとめです。

1.3.1の(i)の"if"の証明を酒井さんが解いて下さったので、その図を載せときます。

まず、示さなきゃいけないのは、問題文のようなhが与えられたとき、(u,f)がCartesianであること。つまり、以下の図の青字のような任意の(v,g):(K,Z)→(J,Y)とwに対して、赤の点線のような射(w,j):(K,Z)→(I,X) が唯一存在することです。

で、このjをhから構成します。構成法は以下の図。まず、青の矢印に注目すると、<π;w,g>:K×Z→I×Yを構成できます。次に、緑の矢印を追っかけていくと、jが構成できます。

でもって、まず、このjについて(w,j);(u,f) = (v,g)を確認します。上の図のjとfを合成するとgとなることを確かめてやります。題意よりhの上下にできている三角形は可換なので、この辺りを使えば示せそうです。

最後、一意性ですけど・・・示せるのかな?(汗 ちょっと面倒かもしれません*1

"only if" の方の証明は、気が向いたらまとめますw → まとめました

Categorical Logic and Type Theory, Volume 141 (Studies in Logic and the Foundations of Mathematics)
0444508538

*1:可換はhがisoでなくても言えそうなので、唯一性の証明でhがisoなことを使いそう