--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tychonoff1.agda	Fri Jun 02 12:12:29 2023 +0900
@@ -0,0 +1,104 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Level
+open import Ordinals
+module Tychonoff1 {n : Level } (O : Ordinals {n})   where
+
+open import logic
+open _∧_
+open _∨_
+open Bool
+
+import OD
+open import Relation.Nullary
+open import Data.Empty
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+import BAlgebra
+open BAlgebra O
+open inOrdinal O
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+import ODC
+open ODC O
+
+open import filter O
+open import ZProduct O
+-- open import maximum-filter O
+
+open Filter
+
+Filter-Proj1 : {P Q : HOD } → 
+     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+      →    Filter {Power P} {P} (λ x → x) 
+Filter-Proj1 = ?
+
+Filter-Proj1-UF : {P Q : HOD } → 
+     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
+      →   (FP :  Filter {Power P} {P} (λ x → x) ) →   ultra-filter FP
+Filter-Proj1-UF = ?
+
+filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
+    → odef x z → odef (ZFP P Q) z
+filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz )
+
+rcf :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx))
+rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly }
+
+Filter-sym : {P Q a : HOD } → ZFP P Q ∋ a → 
+     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+     → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x)
+Filter-sym {P} {Q} {z} pqz F = 
+    record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = ? }  where
+    fqp : HOD
+    fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf  F)
+    fqp<P : fqp ⊆ Power (ZFP Q P)
+    fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = 
+         ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) 
+            (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) 
+    f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q
+    f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 
+      ; x=ψz = ? }  where
+         q⊆ZQP : q ⊆ ZFP Q P
+         q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) 
+         p⊆ZQP : p ⊆ ZFP Q P
+         p⊆ZQP {z} px = q⊆ZQP (p⊆q px)
+         fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp))))
+         fig06 = Replaced1.x=ψz fqp
+         fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
+         fig03 with Replaced1.az fqp 
+         ... | fz = subst (λ k → odef (filter F) k ) ?  fz where
+             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ px → QPq x (subst (λ k → def (HOD.od k) x) (sym *iso) (p⊆q px))))
+             fig07 = ?
+         fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP
+         fig01 x xz  = ? -- 
+         fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
+         fis00 = filter1 F 
+         fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP
+         fis04 = ? 
+         fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP)))
+             (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04))))
+         fis05 = ?
+
+
+
+Filter-sym-UF : {P Q : HOD } → 
+     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
+     → (FQP : Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) )
+     → ultra-filter FQP
+Filter-sym-UF = ?
+
+Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → 
+     (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+      →    Filter {Power Q} {Q} (λ x → x) 
+Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} (Filter-sym pqa F )
+