# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595897158 -32400
# Node ID 59152f16125a6bd7270e67956629752a6c519f1d
# Parent  48ea49494fd13990824b13d227683d0048ad67c6
...

diff -r 48ea49494fd1 -r 59152f16125a OD.agda
--- a/OD.agda	Tue Jul 28 08:35:58 2020 +0900
+++ b/OD.agda	Tue Jul 28 09:45:58 2020 +0900
@@ -460,22 +460,30 @@
 -- 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 = 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
+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 {!!} {!!}) ) ? 
+         ind1 {_} (isuc {x₁} ltd) ox=x = begin
+              nat→ω (ω→nato (isuc ltd) )         
+           ≡⟨⟩
+              Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
+           ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
+              Union (ord→od x₁ , (ord→od x₁ , ord→od x₁))
+           ≡⟨ trans ( sym oiso) ox=x ⟩
+              x 
+           ∎ where
+               open ≡-Reasoning 
+               lemma0 :  x ∋ ord→od x₁
+               lemma0 = {!!}
+               lemma1 : infinite ∋ ord→od x₁
+               lemma1 = {!!}
+               lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
+               lemma with prev {ord→od x₁} lemma0 lemma1
+               ... | t = {!!}
+
 
 
 infixr  200 _∈_