# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595830314 -32400
# Node ID 8c092c04209360e5de9a661061aa2906f9977987
# Parent  77c6123f49eed335d629bbb34b10351834db661d
...

diff -r 77c6123f49ee -r 8c092c042093 BAlgbra.agda
--- a/BAlgbra.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/BAlgbra.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -51,9 +51,9 @@
         lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
-       (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x}))
+       (record { proj1 = case1 refl ; proj2 = d→∋ A A∋x } ))
     lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
-       (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
+       (record { proj1 = case2 refl ; proj2 = d→∋ B B∋x } ))
 
 ∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
@@ -61,7 +61,7 @@
     lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
     lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
     lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
-        record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
+        record { proj1 = d→∋ A (proj1 lt) ; proj2 = d→∋ B (proj2 lt) } }
 
 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
diff -r 77c6123f49ee -r 8c092c042093 LEMC.agda
--- a/LEMC.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/LEMC.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -45,7 +45,7 @@
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
-   t1 = zf.IsZF.power→ isZF A t PA∋t
+   t1 = power→ A t PA∋t
 
 --- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
@@ -110,7 +110,7 @@
                          lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma1 y with ∋-p X (ord→od y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
-                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
                          lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma = ∀-imply-or lemma1
                  have_to_find : choiced (od→ord X)
@@ -148,7 +148,7 @@
                  lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
                  lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
               np : ¬ (p =h= od∅)
-              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (subst (λ k → odef p k) (sym diso) p∋y) p∅ ) 
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) 
               y1choice : choiced (od→ord p)
               y1choice = choice-func p np
               y1 : HOD
diff -r 77c6123f49ee -r 8c092c042093 OD.agda
--- a/OD.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/OD.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -139,20 +139,15 @@
 odef : HOD → Ordinal → Set n
 odef A x = def ( od A ) x
 
--- If we have reverse of c<→o<, everything becomes Ordinal
-o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
-o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-   lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
-   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt))
-   lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
-   lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
-
 _∋_ : ( a x : HOD  ) → Set n
 _∋_  a x  = odef a ( od→ord x )
 
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
+d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
+d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
+
 cseq :  HOD  →  HOD 
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
@@ -170,6 +165,14 @@
 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 ))
 
+-- If we have reverse of c<→o<, everything becomes Ordinal
+o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
+o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+   lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
+   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (d→∋ x lt))
+   lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
+   lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
+
 -- avoiding lv != Zero error
 orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
 orefl refl = refl
@@ -263,7 +266,6 @@
 odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
@@ -287,7 +289,7 @@
 refl-⊆ {A} = record { incl = λ x → x }
 
 od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
-od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (d→∋ x x>z)))
 
 -- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
@@ -315,7 +317,7 @@
 power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
 power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
     lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
-    lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+    lemma y x∋y = incl x⊆A (d→∋ x x∋y)
 
 open import Data.Unit
 
@@ -349,9 +351,6 @@
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 
-d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
-d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
-
 --
 -- If we have LEM, Replace' is equivalent to Replace 
 --
@@ -371,9 +370,9 @@
         umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
         umax< {y} not = lemma (FExists _ lemma1 not ) where
             lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
-            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
+            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (d→∋ (ord→od x) x<y ))
             lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
-            lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
+            lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (d→∋ U x<U)) 
             lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
             lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
             lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
@@ -455,6 +454,18 @@
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
+ord∋eq : {n : Level } {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set n}
+    → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
+    → ( lt : A ∋ i ) → f i lt 
+ord∋eq {n} {A} {i} {f} of lt = subst (λ k → odef A k ) ?  (of (od→ord i) ?)
+
+nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso  {i} lt = ord∋eq {_} {infinite} {i} (λ x lx → lemma lx ) lt where
+   lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x
+   lemma = {!!}
+
 infixr  200 _∈_
 -- infixr  230 _∩_ _∪_
 
@@ -485,7 +496,7 @@
 union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
 union← X z UX∋z =  FExists _ lemma UX∋z where
     lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
-    lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
+    lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } 
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
@@ -525,7 +536,7 @@
 ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
 ∩-≡ {a} {b} inc = record {
    eq→ = λ {x} x<a → record { proj2 = x<a ;
-        proj1 = odef-subst  {_} {_} {b} {x} (inc (odef-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+        proj1 = odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl diso  } ;
    eq← = λ {x} x<a∩b → proj2 x<a∩b }
 -- 
 -- Transitive Set case
@@ -540,12 +551,12 @@
     eq→ lemma-eq {z} w = proj2 w 
     eq← lemma-eq {z} w = record { proj2 = w  ;
         proj1 = odef-subst  {_} {_} {(Ord a)} {z}
-        ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+        ( t→A (d→∋ t w)) refl diso  }
     lemma1 :  {a : Ordinal } { t : HOD }
         → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
     lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
     lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
-    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 
+    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (d→∋ t x<t))) 
     lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
     lemma = sup-o< _ lemma2
 
@@ -591,7 +602,7 @@
     lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
     lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
     lemmad : Ord (osuc (od→ord A)) ∋ t
-    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) 
+    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (d→∋ t lt))) 
     lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
     lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
         lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
diff -r 77c6123f49ee -r 8c092c042093 ODC.agda
--- a/ODC.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/ODC.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -84,7 +84,7 @@
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
-   t1 = zf.IsZF.power→ isZF A t PA∋t
+   t1 = power→ A t PA∋t
 
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (od→ord y)
diff -r 77c6123f49ee -r 8c092c042093 generic-filter.agda
--- a/generic-filter.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/generic-filter.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -134,22 +134,35 @@
 
 postulate f-extensionality : { n m : Level}  → Relation.Binary.PropositionalEquality.Extensionality n m
 
-ω2f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
- 
+ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
+ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
+
+ω→2f≡i0 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i0 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
+ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) ? p
+
 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
 ω→2f-iso X lt = record {
      eq→ = eq1
    ; eq← = eq2
   } where
      eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x
-     eq1 {x} fx = {!!}
+     eq1 {x} fx = {!!} where
+         x-nat : odef infinite x
+         x-nat =  subst (λ k → odef infinite k) diso ( ODC.double-neg-eilm O
+             (power→ infinite _ (ω2∋f (ω→2f X lt)) (d→∋ (fω→2 (ω→2f X lt)) fx ))) 
+         i : Nat
+         i = ω→nat (ord→od x) (d→∋ infinite x-nat)
+         is-i1 : ω→2f X lt i ≡ i1
+         is-i1 = {!!}
      eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x
-     eq2 {x} Xx = {!!}
+     eq2 {x} Xx = {!!} where
+         x-nat : odef infinite x
+         x-nat = {!!}
   
-fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2f f) ≡ f
+fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
 fω→2-iso f = f-extensionality (λ x → eq1 x ) where
-     eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2f f) x ≡ f x
+     eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2∋f f) x ≡ f x
      eq1 x = {!!}