CCC

圏論の方ですね。TL/1 少し飽きた。Cartesian Closed Category 。デカルトも自分の名前がこんなに使われるとは思ってなかったに違いない。

　１ : Obj A
　_*_ : Obj A → Obj A → Obj A
　_^_ : Obj A → Obj A → Obj A

の三つの要素(True と積と Apply かな) があって、

　(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) は True は何からでも推論できるし、それ唯一しかない。(2)は c → a かつ c → a なら a ∧ b　で、逆に c → a ∧ b なら、 c → a かつ c → a 。最後は、

　　a →　c <= b と a ∧ b → c が同じ

というもの。curry 化にも見えるかな。引数二つと a -> b -> c は同じ。

なんだけど、集合で扱おうとするとうまくいかなくて。要素一つの圏と、圏の積を考えた方が良い。圏論はそういうところあって、なんでもかんでも圏でやった方が良いらしい。そういえば、

　　部分圏を定義するには自己関手が簡単

ってのもあった。部分集合とか面倒くさい。

で、これを等式ベースに定義する方法があって、それとこれとが同値なのを示すというのがお題です。

　 １ : Obj A
　 ○ : (a : Obj A ) → Hom A a １
　 _∧_ : Obj A → Obj A → Obj A
　 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
　 π : {a b : Obj A } → Hom A (a ∧ b) a
　 π' : {a b : Obj A } → Hom A (a ∧ b) b
　 _<=_ : (a b : Obj A ) → Obj A
　 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
　 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a

そもそも登場する演算子が多い。さらに等式が...

　 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
　 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ]
　 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ]
　 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ]
　 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
　 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]

ちょっと量多いが、Hom → 等式はできたし、反対もなんとかなりそう。(e1 は圏の公理)

　 http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/a67959bcd44b/CCChom.agda