Product in ZF

結局、ZFいじってたんですが、

　　濃度を定義するのに onto-map 上への写像を定義する
　　そのためには写像を集合の関係で定義する

で、結局、pair から ordered pair を定義する羽目に。そこで、pair が間違ってることを発見。

いや、別な公理を使ったのかも。結局、論理式で、

　　λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y )

とするだけなので、どうってことなくて変更もたいしたことなかったんですが...

その後の ordered pair が迷走することに。論理式つまり一階述語論理で記述すると、ほぼ教科書通り。

なのだが、数学の教科書って、

　　省略しまくり

そして、Agda では省略は許されない。といっても大した量ではないんですけどね。

全部教科書通りというわけにもいかなくて、ZF→ZF ではなく Agda→ZF なので、ZFの集合とAgdaのデータ構造を対応させる感じ。

ordered pair はこんな感じ。

　　<_,_> : (x y : OD) → OD
　　< x , y > = (x , x ) , (x , y )

pair を使って表す感じ。普通は {{x},{x,y}} と書く奴です。これを使って、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

　　ZFProduct : OD
　　ZFProduct = record { def = λ x → ord-pair x }

こんな感じに。これで、pair ox oy が < x , y > に対応します。ox は集合 x に対応する順序数。

これで、直積の性質(射影π1,π2とか、uniqueness)とか示せば良いのだが、射影は簡単

　　pi1 : { p : Ordinal } → ord-pair p → Ordinal
　　pi1 ( pair x y) = x

そのものだ。constructor も普通。introduction とかいう奴ですね。

　　p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
　　p-iso1 {ox} {oy} = pair ox oy

ところが、uniquness (elimination)がわからない。わかってみれば簡単なんだけど。

　　p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
　　p-iso {x} p = ord≡→≡ (lemma p) where
　　 　　lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
　　 　　lemma (pair ox oy) = refl

data の定義が uniqness つまり、 p ≡ od→ord ( < ord→od x , ord→od y > ) を要求してる。そういえば、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

だからな。でも証明の項は、

　　 　　lemma (pair ox oy) = refl

refl は x ≡ x のconstructorだけど。pair の型の unification でそうなるんだけど、気づいたのは4日目の飛行機の中でした。

まぁ、そんなもの。分かんない時は、どんどん横道にそれちゃうんだよな。ま、わからない時には refl って書くのがAgdaだが。

残りは面倒なので気が向いた時にでも。