チコノフの定理はできました

Agda で書くトポロジーで始めたのは一段落。

まず、FのPとQへの射影が超フィルターであることを示す

すると、それぞれに極限x,yがあるので、その直積<x,y>が極限になる

あとは、その極限<x,y>の近傍がFに含まれることを言えばよい

ってわけですが、フィルタの射影が割と面倒だった

Agda の直積は data で書けば良いんですが、集合なので、

　　二つの要素は集合にエンコードされる

具体的には、<x,y>は、{x,{y}} という集合になる。これは pair で書けて (x , x ) , (x , y ) 。

このエンコードで、それぞれを取り出すのを示す必要がある

　　prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )

ってのはずいぶん前にやったんだが、学部1年の頃の

「なんでこんな当たり前のことを証明しないとだめなのか」ってのを、いまさら理解した感じ。

いや、瞬時に理解した人が多いんだろうけど。

さらに、

　　data ZFProduct　(A B : HOD) : (p : Ordinal) → Set n where
　　　　ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )

　　ZFP　: (A B : HOD) → HOD
　　ZFP　A B = record { od = record { def = λ x → ZFProduct A B x　} ... }

　　zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
　　zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a

みたいに、Agda のdataと対応させる必要がある。　これがわけわからない振る舞いで楽しかったです。

射影自体は

　　　　 FPSet : HOD
　　　　 FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))

二段の置換公理でできるんですけど、これがフィルタであることを示すのがそこそこ難しかった。

irr とか HeterogeneousEquality とか...

https://shinji-kono.github.io/zf-in-agda/html/Tychonoff.html