# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595936904 -32400
# Node ID 349d4e7344032435cc548ee886919a8d0876e86b
# Parent  bf409d31184c71d8d55322a5075b1998c16005c6
...

diff -r bf409d31184c -r 349d4e734403 OD.agda
--- a/OD.agda	Tue Jul 28 17:48:28 2020 +0900
+++ b/OD.agda	Tue Jul 28 20:48:24 2020 +0900
@@ -481,6 +481,10 @@
 pair2 : { x y  : HOD  } →  (x , y ) ∋ y
 pair2 = case2 refl
 
+single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
+single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
+single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
+
 empty : (x : HOD  ) → ¬  (od∅ ∋ x)
 empty x = ¬x<0 
 
@@ -504,17 +508,16 @@
    lemma u t with proj1 t
    lemma u t | case1 u=x = o<> (c<→o< {ord→od y} {ord→od u} (proj2 t)) (subst₂ (λ j k → j o< k )
         (trans (sym diso) (trans (sym u=x) (sym diso)) ) (sym diso) x<y ) -- x ≡ od→ord (ord→od u)
-   lemma u t | case2 u=xx = o<> x<y (subst (λ k → k o< x ) diso {!!} )
-         --  x <  y <  u = (x , x ) 
-          --(ordtrans {!!} (subst₂ (λ j k → j o< k ) {!!} {!!} (c<→o< {ord→od y} {ord→od u} (proj2 t))  ) )) where
-         -- lemma1 : od→ord (ord→od u) o< x
-         --  lemma1 = {!!}
+   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (od→ord (ord→od y)) ) (trans (cong (λ k → ord→od k ) u=xx) oiso )  (proj2 t))) x<y where
+       lemma1 : {x y : Ordinal } → (ord→od x , ord→od x ) ∋ ord→od y → x ≡ y    --  y = x ∈ ( x , x ) = u 
+       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq)
+       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq)
 
 ω-prev-eq : {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
 ω-prev-eq {x} {y} eq with trio< x y
-ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = {!!}
+ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
-ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = {!!}
+ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
 
 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
@@ -540,7 +543,7 @@
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
                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 iφ (isuc {y} ltd1) eq = ⊥-elim ( ? )
                lemma3 (isuc ltd) iφ eq = {!!}
                lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
                ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t