CCC の続き

いろいろさぼりながら。

　(1) Hom A a 1 ≈ {*}
　(2) Hom A c (a × b) ≈ (Hom A c a ) × ( Hom A c b )
　(3) Hom A a (c ^ b) ≈ Hom A (a × b) c

ですが、1対1を表す(行って帰ってくる写像二つとその二つが元に戻ることを示す二つの等式)だけでは足りなくて、

　　写像の合同性を表す cong x ≈ y → f x ≈ f y

と、あと二つの naturality ( 可換性 commutativity )が必要でした。たぶん、1-3 全部、natural iso なんでしょう。

cong が必要なのはちょっと不思議。等号が集合としての等しさ(要するに項として等しい)場合は自動的に成立するけど、

　　関係として等号を定義する時には自明でない

らしい。この辺の厳密さが何に影響するかは知らないんですが、仮定に入れてやれば良い。

二つの naturality は結構複雑。(2)の b を b から c への写像 f : b → c あるいは、f : Hom A b c を使って変更するのが
一対一を表す写像と可換というだけなんだけど。(2) は二つの射の組になるのがわかりづらかったかな。
(3) は対象が構造((a × b) c)を持っているので，その中を操作する操作が必要なので複雑になるみたいです。

いや、こんなの難しいうちに入らないか。

次は、λ a → a × b と λ a → a ^ b の組が随伴関手になっているのを示すみたいです。

で、CCC に新しい対象(新しい仮定、あるいは公理)を足すとどうなるかという Polynominal categoriies 、それから、

　　Functional completeness

かな。なんか名前がかっこいい。型なしλ計算がSKIで表されるのがFunctional completenessの一種とか書いてあるんだが、あんまりピンと来ないな。