# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595649268 -32400
# Node ID 19687f3304c9f2d07d2fb6c286e16dcf07048db1
# Parent  8b0715e28b33b8028c5e9283a5e99dc52bdd2b0a
...

diff -r 8b0715e28b33 -r 19687f3304c9 LEMC.agda
--- a/LEMC.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/LEMC.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -126,6 +126,7 @@
          --
          --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
          --
+         -- FIXME : don't use HOD make this level n, so we can remove ε-induction1 
          record Minimal (x : HOD)  : Set (suc n) where
            field
                min : HOD
@@ -157,7 +158,7 @@
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
          Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
          cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (od→ord x )
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
diff -r 8b0715e28b33 -r 19687f3304c9 OD.agda
--- a/OD.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/OD.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -167,6 +167,9 @@
 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 
 odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
 
+odefo→o< :  {X y : Ordinal } → odef (ord→od X) y → y o< X
+odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt ))
+
 -- avoiding lv != Zero error
 orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
 orefl refl = refl
@@ -319,15 +322,15 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
--- level trick (what'a shame)
--- ε-induction1 : { ψ : HOD  → Set (suc n)}
---    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
---    → (x : HOD ) → ψ x
--- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
---      induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
---      induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
---      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
---      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+-- level trick (what'a shame) for LEM / minimal
+ε-induction1 : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
diff -r 8b0715e28b33 -r 19687f3304c9 Ordinals.agda
--- a/Ordinals.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/Ordinals.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -24,6 +24,9 @@
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
+     TransFinite1 : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
 
 record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
@@ -62,6 +65,7 @@
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
+        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
 
         x<nx = IsNext.x<nx (Ordinals.isNext O)
         osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
diff -r 8b0715e28b33 -r 19687f3304c9 filter.agda
--- a/filter.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/filter.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -20,6 +20,7 @@
 open ODAxiom odAxiom
 
 import ODC
+open ODC O
 
 open _∧_
 open _∨_
diff -r 8b0715e28b33 -r 19687f3304c9 generic-filter.agda
--- a/generic-filter.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -60,11 +60,6 @@
      extend : {x : Nat} → (fr : dom f (lift x) ) →  dom g (lift x  )
      feq : {x : Nat} → {fr : dom f (lift x) } →  pmap f (lift x) fr ≡ pmap g (lift x) (extend fr)
 
-record Gf (f : Nat → Two) (p :  PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where
-   field
-     gn  : Nat
-     f<n :  (f ↑ gn) f⊆ p
-
 record FiniteF (p :  PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where
    field
      f-max :  Nat 
@@ -84,60 +79,9 @@
 --     ;  dense-p = λ {p} d → {!!}
 --   }
 
-open Gf
 open _f⊆_ 
 open import Data.Nat.Properties
 
-GF :  (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n})  ) _f⊆_ _f∩_
-GF  f = record {  
-       filter = λ p → Gf f p
-     ; f⊆P = lift OneObj
-     ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
-     ; filter2 = λ {p} {q} fp fq  → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
- } where
-     f1 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
-     f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q  (extend (f<n fp )  x<g) ; feq = λ {x} {fr} → lemma {x} {fr}  } where
-         lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr))
-         lemma {x} {fr} = begin
-             pmap (f ↑ gn fp) (lift x) fr
-            ≡⟨ feq (f<n fp )  ⟩
-             pmap p (lift x) (extend (f<n fp)  fr)
-            ≡⟨ feq p⊆q  ⟩
-             pmap q (lift x) (extend p⊆q  (extend (f<n fp)  fr))
-            ∎  where open ≡-Reasoning 
-     f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf  f p ) → (fq : Gf  f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
-     f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
-            fmin : PFunc (Lift n Nat) (Lift n Two)
-            fmin =  f ↑  (min (gn fp) (gn fq)) 
-            lemma1 : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr
-            lemma1 {x} x<g fr gr = begin
-                   pmap p (lift x) fr 
-                ≡⟨ meq p ⟩
-                   pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
-                ≡⟨ sym (feq (f<n fp)) ⟩
-                   pmap (f ↑  (min (gn fp) (gn fq))) (lift x) x<g
-                ≡⟨ feq (f<n fq) ⟩
-                   pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
-                ≡⟨ meq q ⟩
-                   pmap q (lift x) gr
-                ∎  where open ≡-Reasoning 
-            lemma2  : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift x)
-            lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ;
-                     proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }}
-            f∩→⊆ : (p q : PFunc (Lift n Nat) (Lift n Two) ) → (p f∩ q ) f⊆ q
-            f∩→⊆ p q = record {
-                   extend = λ {x} pq → proj1 (proj2 pq)
-                 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) 
-                }
-            lemma3 :  {x : Nat}  → ( fr : Lift n (x ≤ min (gn fp) (gn fq)))  → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr)
-            lemma3 {x} fr = 
-                  pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr
-                ≡⟨ feq (f<n fq) ⟩
-                  pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
-                ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} )   ⟩
-                  pmap (p f∩ q) (lift x) (lemma2 fr)
-                ∎  where open ≡-Reasoning 
-
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
@@ -200,35 +144,6 @@
 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
 
-record Gfo (x : Ordinal) : Set n where
-  field
-     gfunc : Ordinal
-     gmax : Ordinal
-     gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
-     gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x 
-     pcond : odef HODω2 x
-
-open Gfo
-
-HODGf : HOD
-HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }
-
-G : (Nat → Two) → Filter HODω2
-G f = record {
-       filter = HODGf
-     ; f⊆PL = {!!}
-     ; filter1 = {!!}
-     ; filter2 = {!!}
-   } where
-       filter0 : HOD   
-       filter0 = {!!}
-       f⊆PL1 :  filter0 ⊆ Power HODω2 
-       f⊆PL1 = {!!}
-       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
-       filter11 = {!!}
-       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
-       filter12 = {!!}
-
 -- the set of finite partial functions from ω to 2
 
 Hω2f : Set (suc n)
@@ -244,26 +159,62 @@
        ctl← : Ordinal → Nat
        ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
        ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
+
+record CountableHOD : Set (suc (suc n)) where
+   field
+       phod : HOD
+       ptl→ : Nat → Ordinal
+       ptl→∈P : (i : Nat) → odef phod (ptl→ i)
+       ptl← : (x : Ordinal) → odef phod x → Nat
+       ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x 
+       ptl-iso← : { x : Nat }  → ptl← (ptl→ x ) (ptl→∈P x) ≡ x
+   
        
 open CountableOrdinal 
+open CountableHOD
 
-PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n
-PGOD  i C p q =  ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x →  odef (ord→od q) x ))
+PGHOD : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
+PGHOD P i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (ord→od p) y →  odef (ord→od x) y ) }
+   ; odmax = ctl→ C i  ; <odmax = λ {y} lt → odefo→o< (proj1 lt)}  
+
+next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
+next-p P i C p with ODC.decp O ( PGHOD P i C p =h= od∅ )
+next-p P i C p | yes y = p
+next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD P i C p ) not)
 
-PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
-PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } 
+data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
+    pd0 : PD P C o∅ 0 
+    pdsuc : {p : Ordinal } {i : Nat} → PD P C p i  → PD P C (next-p P i C p) (Suc i) 
+
+record PDN (P : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where
+   field
+       px∈ω : odef (phod P) x
+       pdod : PD P C x (ptl← P x px∈ω)
+
+open PDN
 
-ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal
-ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q )
-ord-compare i C p q | case1 y = p
-ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) 
+PDHOD : (P : CountableHOD ) → (C : CountableOrdinal) → HOD
+PDHOD P C = record { od = record { def = λ x →  PDN P C x }
+    ; odmax = odmax (phod P) ; <odmax = λ {y} lt → <odmax (phod P) (px∈ω lt) } where
+
+--
+--  p 0 ≡ ∅
+--  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
+---             else p n
 
-data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set (suc n) where
-    pd0 : PD P C o∅ 0 
-    -- pdq : {q pnx : Ordinal } {n : Nat}  → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) 
+Gω2r :  (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
+Gω2r  x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} {!!} (ord→od x)) where
+    ψ : HOD  → Set n
+    ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
+    ind : {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) →
+         (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) →
+         (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x)
+    ind {x} prev lt with ω→nat x lt
+    ... | Zero = subst (λ k → Hω2 Zero k) ? hφ
+    ... | Suc t = {!!}
 
-P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P
+P-GenericFilter : {P : CountableHOD } → (C : CountableOrdinal) → GenericFilter (phod P)
 P-GenericFilter {P} C = record {
-      genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+      genf = record { filter = PDHOD P C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    }
diff -r 8b0715e28b33 -r 19687f3304c9 partfunc.agda
--- a/partfunc.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/partfunc.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -209,25 +209,7 @@
       lemma2 (just i1 ∷ p) = lemma2 p
       lemma2 (nothing ∷ p) = lemma2 p
 
-record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where
-   field
-     3gn  : Nat
-     3f<n : p 3⊆ (f 3↑ 3gn)
-
-open 3Gf
-
-min  = Data.Nat._⊓_
+-- min  = Data.Nat._⊓_
 -- m≤m⊔n  = Data.Nat._⊔_
-open import Data.Nat.Properties
+-- open import Data.Nat.Properties
 
-3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_
-3GF {n} f = record {  
-       filter = λ p → 3Gf f p
-     ; f⊆P = OneObj
-     ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
-     ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
- }  where
-      lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
-      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = {!!} }
-      lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
-      lemma2 p q fp fq = ?