# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564749105 -32400
# Node ID f15eaa7c5932e76201879b4957603d914efc99de
# Parent  e05575588191dc6717afee181f2f041e6fe51381
Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y  is bad decision

diff -r e05575588191 -r f15eaa7c5932 OD.agda
--- a/OD.agda	Fri Aug 02 16:27:53 2019 +0900
+++ b/OD.agda	Fri Aug 02 21:31:45 2019 +0900
@@ -308,31 +308,6 @@
     ｛_｝ : ZFSet → ZFSet
     ｛ x ｝ = ( x ,  x )
 
-    u-osuc : { x : Ordinal {suc n}} → Union (ord→od x , (ord→od x , ord→od x )) == ord→od (osuc x)
-    u-osuc {x} = record { eq→ = lemma1 ; eq← = lemma2 } where
-        lemma1 : {y : Ordinal} → def (Union (ord→od x , (ord→od x , ord→od x))) y → def (ord→od (osuc x)) y
-        lemma1 {y} lt = {!!}
-        lemma2 : {y : Ordinal} → def (ord→od (osuc x)) y → def (Union (ord→od x , (ord→od x , ord→od x))) y
-        lemma2 {y} lt not = {!!}
-
-    union-ord : { x : Ordinal {suc n}} → Union (Ord x) == record { def = λ y → osuc y o< x }
-    union-ord {x} = record { eq→ = lemma1 ; eq← = lemma2 } where
-         lemma1 : {y : Ordinal} → def (Union (Ord x)) y → osuc y o< x
-         lemma1 {y} lt with trio< (osuc y) x
-         lemma1 {y} lt | tri< a ¬b ¬c = a
-         lemma1 {y} lt | tri≈ ¬a refl ¬c = ⊥-elim ( lt (λ u → lemma3 {u}) ) where
-             lemma3 : {u : Ordinal} → (u o< osuc y) ∧ def (ord→od u) y → ⊥
-             lemma3 {u} lt with osuc-≡< (proj1 lt)
-             lemma3 {u} lt | case1 refl = o<¬≡ refl (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) (sym diso) refl )
-             lemma3 {u} lt | case2 lt1 = o<> lt1 (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
-         lemma1 {y} lt | tri> ¬a ¬b c = ⊥-elim ( lt (λ u → lemma4 {u} ) ) where
-             lemma4 : {u : Ordinal} → (u o< x) ∧ def (ord→od u) y → ⊥  -- c : x o< osuc y
-             lemma4 {u} lt with osuc-≡< c
-             lemma4 {u} lt | case1 refl = o<> (proj1 lt) (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
-             lemma4 {u} lt | case2 lt1 = o<> ( ordtrans ( proj1 lt)  lt1 ) (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
-         lemma2 : {y : Ordinal} → osuc y o< x → def (Union (Ord x)) y
-         lemma2 {y} lt not = not (osuc y) record { proj1 = lt ; proj2 = {!!} } -- lt :  def (Ord x) (osuc y)
-
     data infinite-d  : ( x : Ordinal {suc n} ) → Set (suc n) where
         iφ :  infinite-d o∅
         isuc : {x : Ordinal {suc n} } →   infinite-d  x  →