# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595910865 -32400
# Node ID f7b844af9a50d5ca00be9a878a267491b25bb0b5
# Parent  ce2ce3f62023c01452897a626d5c541f27d94699
...

diff -r ce2ce3f62023 -r f7b844af9a50 OD.agda
--- a/OD.agda	Tue Jul 28 10:51:08 2020 +0900
+++ b/OD.agda	Tue Jul 28 13:34:25 2020 +0900
@@ -494,7 +494,7 @@
 ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+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
@@ -519,11 +519,24 @@
                   (od→ord (ord→od x₁ , ord→od x₁))  record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
                lemma1 : infinite ∋ ord→od x₁
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
-               lemma2 : {x₁ : Ordinal} → {ltd : infinite-d x₁ } → ω→nato ltd ≡ ω→nat (ord→od x₁) (subst (λ k → odef infinite k) (sym diso) ltd)
-               lemma2 {o∅} {iφ} = {!!}
-               lemma2 {x₁}  {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} )
+               lemma5 : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
+               lemma5 {x} {y} eq = {!!}
+               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
+               lemma3 iφ iφ refl = HE.refl
+               lemma3 iφ (isuc ltd1) eq = {!!}
+               lemma3 (isuc ltd) iφ eq = {!!}
+               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (lemma5 (sym eq))
+               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (lemma5 eq)) t  
+               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
+               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
+                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
+                   lemma6 refl HE.refl = refl
                lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
-               lemma = trans  (cong (λ k →  nat→ω  k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 )
+               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} = {!!}
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t