# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595949907 -32400
# Node ID 3fba5f805e50ca628944ab81233f2ea4b413badb
# Parent  3ac3704b4cb18083f426e69aa89071a8e6c8d13e
nat→ω-iso

diff -r 3ac3704b4cb1 -r 3fba5f805e50 OD.agda
--- a/OD.agda	Tue Jul 28 22:34:42 2020 +0900
+++ b/OD.agda	Wed Jul 29 00:25:07 2020 +0900
@@ -522,6 +522,9 @@
 ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
 ω-∈s x not = not (od→ord (x , x)) record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord x) ) (sym oiso) (case1 refl) }
 
+ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
+ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → od→ord y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (od→ord y )) eq (ω-∈s y) ))) )
+
 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) →
@@ -558,8 +561,16 @@
                lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym diso) ltd)  diso ) ) ( prev {ord→od x₁} lemma0 lemma1 )
 
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {Zero} = {!!}
-ω→nat-iso {Suc i} = {!!}
+ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) oiso where
+   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → ord→od x ≡  nat→ω i → ω→nato ltd ≡ i
+   lemma {x} Zero iφ eq = refl
+   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
+   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (ord→od x) (subst (λ k → k ≡ od∅  ) oiso eq ))
+   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- ord→od x ≡ nat→ω i
+           lemma1 :  ord→od (od→ord (Union (ord→od x , (ord→od x , ord→od x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → ord→od x ≡ nat→ω i
+           lemma1 eq = subst (λ k → ord→od x ≡ k ) oiso (cong (λ k → ord→od k)
+                ( ω-prev-eq (subst (λ k → _ ≡ k ) diso (cong (λ k → od→ord k ) (sym
+                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym oiso ) eq ))))))
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t