# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1676688682 -32400
# Node ID 375615f9d60f893735d033e02594f36ed114758f
# Parent  4b2f49a5a1d5843500662c658daaf24dcddec70a
Func and Funcs

diff -r 4b2f49a5a1d5 -r 375615f9d60f src/PFOD.agda
--- a/src/PFOD.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/PFOD.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -144,17 +144,6 @@
         le03 :  x ≡ & (nat→ω (ω→nato wx))
         le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
 
-¬i0≡i1 : ¬ ( i0 ≡ i1 )
-¬i0≡i1 ()
-
-¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 
-¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
-¬i0→i1 {i1} ne = refl
-
-¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
-¬i1→i0 {i0} ne = refl
-¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
-
 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f
 fω→2-iso f = f-extensionality (λ x → le01 x ) where
     le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
diff -r 4b2f49a5a1d5 -r 375615f9d60f src/Tychonoff.agda
--- a/src/Tychonoff.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/Tychonoff.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -79,6 +79,9 @@
      N∋nc = ?
      0<PP : o∅ o< & (Power P)
      0<PP = ?
+     --
+     -- FIP defines a filter
+     --
      F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
      F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
          f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
@@ -102,19 +105,31 @@
               f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
               f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
                  → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
+     --
+     -- it contains no empty sets
+     -- 
      proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
      proper = ?
+     --
+     -- then we have maximum ultra filter 
+     --
      maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
      maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} CSX fp =  MaximumFilter.mf (maxf CSX fp) 
      ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
      ultraf {X} CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
+     --
+     -- so i has a limit as a limit of UIP
+     --
      limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
      limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
      uf02 : {X v  : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
         → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
      uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf CSX fp)) nei vx
+     --
+     -- the limit is an element of entire elements of X
+     --
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
      uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp))
      ... | yes y = subst (λ k → odef (* x) k) &iso y
@@ -136,16 +151,28 @@
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
+     --
+     -- take closure of given filter elements
+     --
      CF : HOD
      CF = Replace' (filter F) (λ x fx → Cl TP x  )
      CF⊆CS : CF ⊆ CS TP
      CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 
+     --
+     -- it is set of closed set and has FIP ( F is proper )
+     --
      ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
      ufl01 = ?
+     --
+     -- so we have a limit
+     --
      limit : Ordinal
      limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
      ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
      ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
+     --
+     -- Neigbor of limit ⊆ Filter
+     --
      ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅  -- because limit is in CF which is a closure
      ufl03 {f} {v} ff nei fv=0 = ?
      pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
@@ -211,7 +238,7 @@
                  nei1 : HOD
                  nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
                  plimit : Ordinal
-                 plimit = UFLP.limit uflp ? 
+                 plimit = UFLP.limit uflp 
                  nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
                  nproper = ?
                  b∋z : odef nei1 z
diff -r 4b2f49a5a1d5 -r 375615f9d60f src/cardinal.agda
--- a/src/cardinal.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/cardinal.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -45,14 +45,28 @@
 -- _⊗_ : (A B : HOD) → HOD
 -- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
-Func :  OD
-Func = record { def = λ x → def ZFPair x
-    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }
+record Func (A B : HOD) : Set n where
+    field
+       func : Ordinal → Ordinal
+       is-func : {x : Ordinal } → odef A x → odef B (func x)
+
+data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace A ( λ x → < x , (* (Func.func F (& x))) > )))
+
+FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
+FuncHOD→F {A} {B} (felm F) = F
 
-FuncP :  ( A B : HOD ) → HOD
-FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
-    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 ? ≡ pi1 ? → pi2 ? ≡ pi2 ? ) }
-       ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
+FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
+FuncHOD=R {A} {B}  (felm F) = *iso
+
+Funcs : (A B : HOD) → HOD
+Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B)) 
+       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
+    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (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 → odef (A ⊗ B) k ) (sym x=ψz) (
+       product→ (subst (λ k → odef A k) (sym &iso) az) (subst (λ k → odef B k) 
+         (trans (cong (Func.func F) (sym &iso)) (sym &iso)) (Func.is-func F az) ))
 
 record Injection (A B : Ordinal ) : Set n where
    field
diff -r 4b2f49a5a1d5 -r 375615f9d60f src/generic-filter.agda
--- a/src/generic-filter.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/generic-filter.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -61,7 +61,8 @@
        ctl<M : (x : Nat) → odef (ctl-M) (ctl→ x) 
        ctl← : (x : Ordinal )→  odef (ctl-M ) x → Nat
        ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x )  → ctl→ (ctl← x lt ) ≡ x 
-       ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
+       -- we have no otherway round
+       -- ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
 --
 -- almmost universe
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
@@ -241,6 +242,14 @@
     D = ?
 
 --
+-- P-Generic Filter defines a countable model D ⊂ C from P
+--
+
+--
+-- in D, we have V ≠ L
+--
+
+--
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
 
diff -r 4b2f49a5a1d5 -r 375615f9d60f src/logic.agda
--- a/src/logic.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/logic.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -50,6 +50,19 @@
 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
 dont-orb {A} {B} (case1 a) ¬B = a
 
+open import Relation.Binary.PropositionalEquality
+
+¬i0≡i1 : ¬ ( i0 ≡ i1 )
+¬i0≡i1 ()
+
+¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 
+¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
+¬i0→i1 {i1} ne = refl
+
+¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
+¬i1→i0 {i0} ne = refl
+¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
+
 
 infixr  130 _∧_
 infixr  140 _∨_