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

diff -r 59152f16125a -r d87492ae4040 OD.agda
--- a/OD.agda	Tue Jul 28 09:45:58 2020 +0900
+++ b/OD.agda	Tue Jul 28 10:32:33 2020 +0900
@@ -389,6 +389,14 @@
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
+union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
+    ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
+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 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } 
+
 data infinite-d  : ( x : Ordinal  ) → Set n where
     iφ :  infinite-d o∅
     isuc : {x : Ordinal  } →   infinite-d  x  →
@@ -456,36 +464,6 @@
 _=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
-
-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 {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 _∈_
 -- infixr  230 _∩_ _∪_
 
@@ -497,6 +475,12 @@
 pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
 pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
 
+pair1 : { x y  : HOD  } →  (x , y ) ∋ x
+pair1 = case1 refl
+
+pair2 : { x y  : HOD  } →  (x , y ) ∋ y
+pair2 = case2 refl
+
 empty : (x : HOD  ) → ¬  (od∅ ∋ x)
 empty x = ¬x<0 
 
@@ -510,13 +494,34 @@
 ⊆→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 ))
 
-union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
-    ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
-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 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } 
+-- 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} = ε-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 {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 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not 
+                  (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
+               lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
+               lemma with prev {ord→od x₁} lemma0 lemma1
+               ... | t = {!!}
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t