--- a/ordinal-definable.agda	Sat Jun 01 10:23:53 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 14:43:05 2019 +0900
@@ -331,9 +331,9 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = {!!}
-       ;   union→ = {!!}
-       ;   union← = {!!}
+       ;   union-u = union-u
+       ;   union→ = union→
+       ;   union← = union←
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
@@ -353,19 +353,19 @@
          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 | osuc (od→ord z )
-         union-u X z (case1 (s≤s z≤n)) | record { lv = .(Suc _) ; ord = ord₁ } | record { lv = .0 ; ord = ord₂ } = {!!}
-         union-u X z (case1 (s≤s (s≤s x))) | record { lv = .(Suc (Suc _)) ; ord = ord₁ } | record { lv = .(Suc _) ; ord = ord₂ } = {!!}
-         union-u X z (case2 Φ<) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(Φ lv₁) } = {!!}
-         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 _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } = {!!}
-         union-u X z (case2 (ℵ< x)) | record { lv = .(Suc _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } = {!!}
-         union-u X z (case2 ℵs<) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
-         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← :  (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← = {!!}
+         union-u X z U>z = ord→od ( osuc ( od→ord z ) )
+         union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
+         union-lemma-u {X} {z} U>z = lemma <-osuc where
+             lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
+             lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
+         union→ :  (X z u : OD) → (Union X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
+         union→ X y u xx | tri< a ¬b ¬c = {!!}
+         union→ X y u xx | tri≈ ¬a b ¬c = {!!}
+         union→ X y u xx | tri> ¬a ¬b c = {!!}
+            --  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
+         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
+         union← X z X∋z = record { proj1 = {!!} ; proj2 = union-lemma-u X∋z }
          ψ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)