# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595892958 -32400
# Node ID 48ea49494fd13990824b13d227683d0048ad67c6
# Parent  03a4e1b8f3fb72ffd36460f1407e9117824b1897
use induction

diff -r 03a4e1b8f3fb -r 48ea49494fd1 OD.agda
--- a/OD.agda	Mon Jul 27 19:58:46 2020 +0900
+++ b/OD.agda	Tue Jul 28 08:35:58 2020 +0900
@@ -407,6 +407,9 @@
 -- infinite : HOD 
 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
+odsuc : (y : HOD) → HOD
+odsuc y = Union (y , (y , y))
+
 infinite : HOD 
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
     u : (y : Ordinal ) → HOD
@@ -437,11 +440,12 @@
 nat→ω Zero = od∅
 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
 
+ω→nato : {y : Ordinal} → infinite-d y → Nat
+ω→nato iφ = Zero
+ω→nato (isuc lt) = Suc (ω→nato lt)
+
 ω→nat : (n : HOD) → infinite ∋ n → Nat
-ω→nat n = lemma where
-    lemma : {y : Ordinal} → infinite-d y → Nat
-    lemma iφ = Zero
-    lemma (isuc lt) = Suc (lemma lt)
+ω→nat n = ω→nato 
 
 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
@@ -452,40 +456,27 @@
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
-
-
-ord∋eq :  {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set (suc n)}
-    → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
-    → ( lt : A ∋ i ) → f i lt 
-ord∋eq {A} {i} {f} of lt = lemma oiso lt where
-   lemma2 : (j : Ordinal) → (ltj :  odef A j )
-          → (i : HOD) → (lti :  odef A (od→ord i) )
-          →  (ord→od j ≡ i ) →  d→∋ A ltj ≅ lti
-   lemma2 j _ i _ refl = HE.refl 
-   lemma1 : (j : Ordinal) → (ltj :  odef A j )
-          → (i : HOD) → (lti :  odef A (od→ord i) )
-          →  (ord→od j ≡ i ) →  d→∋ A ltj ≅ lti
-          → f (ord→od j) (d→∋ A ltj) ≡ f i lti
-   lemma1 j _ i _ refl HE.refl = refl
-   lemma0 : (j : Ordinal) → (lt :  odef A j ) → f (ord→od j) (d→∋ A lt) 
-   lemma0 j  lt = of j lt
-   lemma : {i : HOD } → {j : Ordinal} → ord→od j ≡ i  → (lti : odef A (od→ord i)) → f i lti
-   lemma {i} {j} refl lt = subst (λ k → f (ord→od j) k ) {!!} ( of j (subst (λ k → odef A k ) diso lt ))
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
 
 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 {o∅} iφ = begin
-         nat→ω (ω→nat (ord→od o∅) (d→∋ infinite iφ))
-      ≡⟨ {!!} ⟩
-         nat→ω Zero
-      ≡⟨ sym o∅≡od∅ ⟩
-          ord→od o∅ 
-      ∎ where open ≡-Reasoning
-   lemma {x1} (isuc lx) = {!!}
-   
+nat→ω-iso  {i} lt = lemma lt i (sym oiso) od∅ iφ (sym o∅≡od∅) init  where
+     init : nat→ω ( ω→nato iφ ) ≡ od∅
+     init = refl
+     lemma : {x y : Ordinal } → (ltd : infinite-d x ) → (xi : HOD) → xi ≡ ord→od x
+                                → (pi : HOD) → (prev : infinite-d y  ) → pi ≡ ord→od y → nat→ω (ω→nato prev) ≡ pi
+                                → nat→ω (ω→nato ltd) ≡ xi
+     lemma {x} {y} ltd xi xi=x p pi prev pi=p = {!!}
+
+nat→ω-iso' : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso' {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
+     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
+                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
+     ind {x} prev lt = ind1 lt oiso where
+         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x
+         ind1 {o∅} iφ refl = sym o∅≡od∅
+         ind1 (isuc ltd) ox=x = trans (cong (λ k → odsuc k ) (prev {!!} {!!}) ) ? 
+
 
 infixr  200 _∈_
 -- infixr  230 _∩_ _∪_
diff -r 03a4e1b8f3fb -r 48ea49494fd1 generic-filter.agda
--- a/generic-filter.agda	Mon Jul 27 19:58:46 2020 +0900
+++ b/generic-filter.agda	Tue Jul 28 08:35:58 2020 +0900
@@ -139,7 +139,7 @@
 
 ω→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≡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 {