Cartesian closed かつ distributive な圏で x × x = x ² を示す

違った方面から攻めてみた。~~なんか途中。~~tex の frac を使ったので見づらい。
[tex: \frac{\large X \to^{} A \times A} {\frac{\large X \to^f A \hspace{4em} X \to^g A} {\frac{\large X + X \to^{\[f,g\]} A} {\frac{\large (X \times 1) + (X \times 1) \to^{\[f,g\]} A} {\frac{\large X \times (1+1) \to^{\[f,g\]'} A}{\large X \longrightarrow^{\small curry(\[f,g\]')} A^2}] ただし、 $X \times (1 + 1) \simeq (X \times 1) + (X \times 1)$ 。
ここから、 $hom(-,A \times A) \simeq hom(-, A^2)$ 。
$h = hom(-,A \times A), \hspace{3em} h' = hom(-, A^2)$ とおくと、米田の補題を使って
$I^{op}(A \times A) \simeq nat(h, I^{op}) \simeq nat(h', I^{op}) \simeq I^{op}(A^2)$
(ただし、 $I^{op} : C \to C^{op}$ は、対象を保存し、射の向きを反対にするだけの反変関手）。∴ $A \times A \simeq A^2$ 。