よくわからん事

Pierce 本に書いてあったことで、初見では諦めてた問題×2。やっぱり解けない。一見簡単そうなんだけどなあ…? 本の中での扱いも小さいし。

Find a small finite cartesian category that is not cartesian closed.
CCC では常に A^1 と A は isomorphic か。証明か反例。

一個目については対象が有限個なのか射も有限個なのか書いてない。両方有限でやってたけど、一向に見つからない…っていうか今気づいたけどこの「小さい」って「図示できる程度の大きさ」とかそういう意味じゃなくて、「類が出てこない」って意味での「小さい」か、もしかして。射も有限なら存在しないとかいうオチがついてきたら泣く。

二個目は、η簡約みたいなもん。1 が singleton な事を使うからもっとタチ悪いけど。

追記: ああ、やっぱり二個目は楽勝やった。一旦解けてしまうと何で詰まってたのかわからん。

$(\forall X) t_X : X \rightarrow 1$ として、 $A\times 1$ の射影を $\pi_l : A\times 1 \rightarrow A$ , $\pi_r : A \times 1 \rightarrow 1 = t_{A\times 1}$ で $f := curry (\pi_l)$ と置く。Exponentiation についてくる射を $eval : A^1 \times 1 \rightarrow A$ として、[tex:eval \circ *1 = \pi_l \circ \langle id_A, t_A \rangle \circ eval = eval] だから普遍性により $(f \times id_1) \circ (eval \circ \langle id_A, t_A \rangle) = id_{A^1\times 1}$ 。逆に合成して $(\langle id_A, t_A \rangle \circ eval) \circ (f \times id_1)$ $=$ $\langle id_A, t_A \rangle \circ pi_l$ $=$ $\langle pi_l, t_A \circ pi_l \rangle$ $=$ $\langle pi_l, t_{A\times 1} \rangle$ $=$ $\langle pi_l, pi_r \rangle$ $=$ $id_{A\times 1}$

*1:f \times id_1) \circ (eval \circ \langle id_A, t_A \rangle