--- a/ordinal-definable.agda	Wed Jun 05 09:47:19 2019 +0900
+++ b/ordinal-definable.agda	Wed Jun 05 14:35:32 2019 +0900
@@ -33,7 +33,7 @@
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
-_c<_ : { n : Level } → ( a x : OD {n} ) → Set n
+_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
 x c< a = a ∋ x 
 
 record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
@@ -136,6 +136,7 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
+
 =→¬< : {x : Nat  } → ¬ ( x < x )
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
@@ -166,6 +167,17 @@
 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
 
+≡-def : {n : Level} →  { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } )
+≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
+    lemma :  ord→od x == record { def = λ z → z o< x }
+    eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso diso t where 
+         t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
+         t = c<→o< {suc n} {ord→od w} {ord→od x} (def-subst {suc n} {_} {_} {ord→od x} {_} z refl (sym diso))
+    eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} ( o<→c< {suc n} {_} {_} z ) refl diso
+
+od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
+od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
+
 ¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
 ¬x<0 {n} {x} (case1 ())
 ¬x<0 {n} {x} (case2 ())
@@ -352,6 +364,10 @@
          xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
              lemma : {x  : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
              lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} )
+         uxxx-union : {x  : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
+         uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k } ) lemma where
+             lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
+             lemma = {!!}
          infinite : OD {suc n}
          infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
          infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1  } ) ∋ od∅ {suc n}