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" の方の証明は、気が向いたらまとめますｗ → まとめました。
Categorical Logic and Type Theory, Volume 141 (Studies in Logic and the Foundations of Mathematics)
*1:可換はhがisoでなくても言えそうなので、唯一性の証明でhがisoなことを使いそう
