# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680501756 -32400
# Node ID b15dd4438d504d783e9a07680e48af9f99df595a
# Parent  30540f151ae0fd59a3a330d050bb7c73fc8e4de7
...

diff -r 30540f151ae0 -r b15dd4438d50 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Apr 02 12:41:06 2023 +0900
+++ b/src/Tychonoff.agda	Mon Apr 03 15:02:36 2023 +0900
@@ -35,7 +35,7 @@
 open import filter O
 open import ZProduct O
 open import Topology O
-open import maximum-filter O
+-- open import maximum-filter O
 
 open Filter
 open Topology
@@ -176,11 +176,11 @@
      --    otherwise the check requires a minute
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     maxf {X} 0<X CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
      ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      --
      -- so it has a limit as a limit of UIP
      --
@@ -345,6 +345,17 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
+FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+     → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
+FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
+
+projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+     → Filter {Power P} {P} (λ x → x) 
+projection-of-filter = ?
+
+projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
+     → ultra-filter (projection-of-filter F)
+projection-of-ultra-filter = ?
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
diff -r 30540f151ae0 -r b15dd4438d50 src/ZProduct.agda
--- a/src/ZProduct.agda	Sun Apr 02 12:41:06 2023 +0900
+++ b/src/ZProduct.agda	Mon Apr 03 15:02:36 2023 +0900
@@ -104,48 +104,6 @@
 ZFPair : OD
 ZFPair = record { def = λ x → ord-pair x }
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
--- eq-pair refl refl = HE.refl
-
-pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi1 ( pair x y) = x
-
-π1 : { p : HOD } → def ZFPair (& p) → HOD
-π1 lt = * (pi1 lt )
-
-pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi2 ( pair x y ) = y
-
-π2 : { p : HOD } → def ZFPair (& p) → HOD
-π2 lt = * (pi2 lt )
-
-op-cons :  ( ox oy  : Ordinal ) → def ZFPair (& ( < * ox , * oy >   ))
-op-cons ox oy = pair ox oy
-
-def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
-def-subst df refl refl = df
-
-p-cons :  ( x y  : HOD ) → def ZFPair (& ( < x , y >))
-p-cons x y = def-subst {_} {_} {ZFPair} {& (< x , y >)} (pair (& x) ( & y )) refl (
-   let open ≡-Reasoning in begin
-       & < * (& x) , * (& y) >
-   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
-       & < x , y >
-   ∎ ) 
-
-op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
-op-iso (pair ox oy) = refl
-
-p-iso :  { x  : HOD } → (p : def ZFPair (&  x) ) → < π1 p , π2 p > ≡ x
-p-iso {x} p = ord≡→≡ (op-iso p) 
-
-p-pi1 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π1 p ≡ x
-p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
-
-p-pi2 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π2 p ≡ y
-p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
-
 _⊗_ : (A B : HOD) → HOD
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
@@ -196,16 +154,6 @@
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
 ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
 
-⊗⊆ZFPair : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFPair (& x)
-⊗⊆ZFPair {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = aa ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
-       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
-       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
-       zfp01 : def ZFPair (& x)
-       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
-       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ  k → def ZFPair  k) (cong (&) zfp00) (op-cons b a )  where
-           zfp00 : < * b , * a > ≡ x
-           zfp00 = sym ( subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψb) )
-
 ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
 ⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
        zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
@@ -228,6 +176,81 @@
 ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
 
+record Func (A B : HOD) : Set n where
+    field
+       func : {x : Ordinal } → odef A x → Ordinal
+       is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
+
+data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > )))
+
+FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
+FuncHOD→F {A} {B} (felm F) = F
+
+FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > )
+FuncHOD=R {A} {B}  (felm F) = *iso
+
+--
+--  Set of All function from A to B
+--
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
+Funcs : (A B : HOD) → HOD
+Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) 
+       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where
+    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x
+    lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
+    ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) 
+          (sym x=ψz) lemma4 where
+       lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > )
+       lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az))
+
+record Injection (A B : Ordinal ) : Set n where
+   field
+       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
+       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
+       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
+
+record OrdBijection (A B : Ordinal ) : Set n where
+   field
+       fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
+       fun→  : (x : Ordinal ) → odef (* B)  x → Ordinal
+       funB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( fun← x lt )
+       funA  : (x : Ordinal ) → ( lt : odef (* B)  x ) → odef (* A) ( fun→ x lt )
+       fiso← : (x : Ordinal ) → ( lt : odef (* B)  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
+       fiso→ : (x : Ordinal ) → ( lt : odef (* A)  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
+
+ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
+ordbij-refl {a} refl = record {
+       fun←  = λ x _ → x 
+     ; fun→  = λ x _ → x 
+     ; funB  = λ x lt → lt
+     ; funA  = λ x lt → lt
+     ; fiso← = λ x lt → refl
+     ; fiso→ = λ x lt → refl
+    }
+
+ZFPsym : (A B  : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A))
+ZFPsym A B = record {
+       fun←  = λ xy ab → & < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) > 
+     ; fun→  = λ xy ba → & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > 
+     ; funB  = λ xy ab → subst (λ k → odef k (&
+             < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) >)) 
+          (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ab)) (zp1 (subst (λ k → odef k xy) *iso ab))  )
+     ; funA  = λ xy ba → subst (λ k → odef k (&
+             < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >)) 
+          (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ba)) (zp1 (subst (λ k → odef k xy) *iso ba))  )
+     ; fiso← = λ xy ba → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 {A} {B} {zπ2 (subst (λ k → odef k xy) *iso ba)} {zπ1 (subst (λ k → odef k xy) *iso ba)} (lemma1 ba) )) 
+       ? ) ( zp-iso (subst (λ k → odef k xy) *iso ba )) 
+     ; fiso→ = λ xy ab → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 ? )) (proj1 (zp-iso0 ? ))  ) ( zp-iso (subst (λ k → odef k xy) *iso ab )) 
+    } where
+        lemma1 : {A B : HOD} {xy : Ordinal} → (ba : odef (* (& (ZFP B A))) xy) → odef (ZFP A B) (
+                & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >  )
+        lemma1 {A} {B} {xy} ba = ? -- with subst (λ k → odef k xy ) *iso ba
+        -- ... | ab-pair ax by = ?
+
+
 ZFP∩  : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A  ∩ ZFP C B )
 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00  ; eq← = zfp01 } where
    zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x