# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564290428 -32400
# Node ID 9eb6a8691f02a466f0910533a5c749e87b15bf71
# Parent  6e778b0a720244cb0575317836fd9ce5cf4d3c73
choice function cannot jump between ordinal level

diff -r 6e778b0a7202 -r 9eb6a8691f02 OD.agda
--- a/OD.agda	Fri Jul 26 21:08:06 2019 +0900
+++ b/OD.agda	Sun Jul 28 14:07:08 2019 +0900
@@ -238,10 +238,10 @@
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
 
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
-Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→
+Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
 
 
 _⊆_ : {n : Level} ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
@@ -255,11 +255,6 @@
     ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
    } 
 
-Def=A→Set : {n : Level} → (A  :  Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n  }
-Def=A→Set {n} A  = record {
-              eq→ = λ {y} DAx y<A →  {!!}
-        ;  eq← = {!!} -- λ {y} f → {!!}
-    } where
 
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
@@ -505,7 +500,16 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
-         -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
+         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
+         choice-func' X ∋-p not = lemma (lv (od→ord X )) (ord (od→ord X)) where
+             lemma : (lx : Nat ) ( ox : OrdinalD lx )  → OD {suc n}
+             lemma lx ox  with ∋-p X (ord→od record { lv = lx ; ord = ox })
+             lemma lx ox | yes p = (ord→od record { lv = lx ; ord = ox })
+             lemma Zero (Φ 0)  | no ¬p = od∅
+             lemma Zero (OSuc 0 ox)  | no ¬p = lemma  Zero ox 
+             lemma (Suc lx) (Φ (Suc lx))  | no ¬p = {!!}
+             lemma (Suc lx) (OSuc (Suc lx) ox)  | no ¬p = lemma ( Suc lx ) ox 
+
          --
          -- another form of regularity 
          --
diff -r 6e778b0a7202 -r 9eb6a8691f02 filter.agda
--- a/filter.agda	Fri Jul 26 21:08:06 2019 +0900
+++ b/filter.agda	Sun Jul 28 14:07:08 2019 +0900
@@ -10,6 +10,8 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 open import  Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
 
 record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
    field
@@ -24,6 +26,20 @@
 dense :  {n : Level} → Set (suc (suc n))
 dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
 
+record NatFilter {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+   field
+       GN : Nat → Set n
+       GN∋1 : GN 0
+       GNmax : { p : Nat } → P p →  0 ≤ p 
+       GNless : { p q : Nat } → GN p → P q →  q ≤ p  → GN q
+       Gr : (  p q : Nat ) →  GN p → GN q  →  Nat
+       GNcompat : { p q : Nat }  → (gp : GN p) → (gq : GN q ) → (  Gr p q gp gq ≤  p ) ∨ (  Gr p q gp gq ≤ q )
+
+record NatDense {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+   field
+       Gmid : { p : Nat } → P p  → Nat
+       GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) →  Gmid pp  ≤ p 
+
 open OD.OD
 
 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
@@ -36,12 +52,9 @@
 Hω2 : {n : Level} →  OD {suc n}
 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
 
-_⊆_ : {n : Level} → ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
-_⊆_ A B {x} = A ∋ x →  B ∋ x
-
 Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
 Hω2Filter {n} = record {
-       _⊇_ = {!!}
+       _⊇_ = _⊇_
      ; G = {!!}
      ; G∋1 = {!!}
      ; Gmax = {!!}