--- a/ordinal-definable.agda	Fri May 31 22:30:23 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 10:01:38 2019 +0900
@@ -332,7 +332,8 @@
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
        ;   union-u = {!!}
-       ;   union-iso = {!!}
+       ;   union→ = {!!}
+       ;   union← = {!!}
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
@@ -351,18 +352,29 @@
          proj2 (pair A B ) =  case2 refl 
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
+         union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
+         union-u X z U>z with od→ord X | od→ord z 
+         union-u X z (case1 (s≤s x)) | record { lv = Suc lX ; ord = oX } | record { lv = lz ; ord = oz } = ord→od (mid (Suc lX) lz oX oz (s≤s x) )  where
+             mid : (lX lz : Nat) → (oX : OrdinalD {suc n} lX ) → (oz : OrdinalD {suc n} lz ) → lX > lz  → Ordinal {suc n}
+             mid (Suc lX) 0 oX oz (s≤s z≤n) = record { lv = 0 ; ord = OSuc 0 oz }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (Φ (Suc lz)) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (Φ (Suc lz) ) }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (OSuc (Suc lz) oz) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (OSuc (Suc lz) oz) }
+             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (ℵ lz) (s≤s (s≤s lt)) = record { lv = (Suc (Suc lX)) ; ord = OSuc (Suc (Suc lX)) (ℵ (Suc lX)) }
+             mid (Suc (Suc lX)) (Suc lz) (OSuc (Suc (Suc lX)) oX) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = oX }
+             mid (Suc (Suc lX)) (Suc lz) (ℵ (Suc lX)) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = OSuc (Suc (Suc lX)) (Φ (Suc (Suc lX))) }
+         union-u X z (case2 Φ<) | record { lv = Zero ; ord = (OSuc 0 oX) } | record { lv = .0 ; ord = .(Φ 0) } =
+             ord→od (record { lv = Zero ; ord = oX }) -- this case contains X = odΦ
+         union-u X z (case2 Φ<) | record { lv = Suc lv₁ ; ord = (OSuc (Suc lv₁) oX) } | record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) } =  ord→od (record { lv = Suc lv₁ ; ord = oX } )
+         union-u X z (case2 (s< x)) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(OSuc lv₁ _) } = {!!}
+         union-u X z (case2 ℵΦ<) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } =  ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (Φ (Suc lX))} )
+         union-u X z (case2 (ℵ< x)) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = OSuc (Suc _) oz } =
+              ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (OSuc (Suc lX) (OSuc (Suc lX) oz ))} )
+         union-u X z (case2 ℵs<) | record { lv = Suc lX ; ord = OSuc (Suc lX) (ℵ lX) } | record { lv = Suc lX ; ord = ℵ lX } = {!!}
+         union-u X z (case2 (ℵss< x)) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
          union→ :  (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
          union→ X x y X∋x x∋y =  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
-         union-u : (X z : OD {suc n}) → OD {suc n}
-         union-u X z = record { def =  ( λ u → (u o< od→ord X)  ∧ (od→ord z o< u) ) }
-         union-iso :  (X z : OD {suc n}) → (Union X ∋ z) ⇔ ((Union X ∋ union-u X z ) ∧ (union-u X z ∋ z))
-         --    ((x : OD) →  (z ∋ x → y ∋ x)) → y ∋ z 
-         proj1 ( union-iso X z ) U∋z = record { proj1 = U∋u ;  proj2 = u∋z } where
-             U∋u : Union X ∋ union-u X z
-             U∋u = {!!}
-             u∋z : union-u X z ∋ z
-             u∋z = {!!}
-         proj2 (union-iso X z ) U∋u∧U∋z  = transitive {n} {!!} {!!} -- (proj1 U∋u∧U∋z ) (proj2 U∋u∧U∋z )
+         union← :  (X z : OD {suc n}) → (X∋z : Union X ∋ z) → ((Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z))
+         union← = {!!}
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)