# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562577596 -32400
# Node ID f0fa9a755513c5a32dc9df7b46d30823b91bef04
# Parent  3ba37037faf44a9ee13c43a0a660d033b0cc2dba
all done but ...

diff -r 3ba37037faf4 -r f0fa9a755513 HOD.agda
--- a/HOD.agda	Mon Jul 08 13:21:14 2019 +0900
+++ b/HOD.agda	Mon Jul 08 18:19:56 2019 +0900
@@ -300,18 +300,15 @@
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
+    A ∩ B = record { def = λ x → def A x ∧ def B x } 
     Union : OD {suc n} → OD {suc n}
-    Union U = Replace ( record { def = λ x → osuc x o< od→ord U } )  ( λ x → U ∩ x ) 
-    -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
+    Union U = record { def = λ y  → def U (osuc y) }
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
-    -- _∪_ : ( A B : ZFSet  ) → ZFSet
-    -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     ｛_｝ : ZFSet → ZFSet
     ｛ x ｝ = ( x ,  x )
 
@@ -346,21 +343,26 @@
          empty x (case1 ())
          empty x (case2 ())
 
-         union-lemma : {n : Level } {X z u : OD {suc n} } → (X ∋ u) → (u ∋ z) → osuc ( od→ord z ) o< od→ord u → X ∋ Ord (osuc ( od→ord z ) )
-         union-lemma = {!!}
+         union-d : (X : OD {suc n}) → OD {suc n}
+         union-d X = record { def = λ y → def X (osuc y) }
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
          union→ X z u xx | tri< a ¬b ¬c | ()
-         union→ X z u xx | tri≈ ¬a b ¬c = {!!}
-         union→ X z u xx | tri> ¬a ¬b c = {!!}  --- osuc ( od→ord z )) o<  od→ord u o< od→ord X
-            -- def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (union-lemma {n} {X} {z} {u} (proj1 xx) (proj2 xx) c ) refl (sym ord-Ord)
+         union→ X z u xx | tri≈ ¬a b ¬c =  def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b
+         union→ X z u xx | tri> ¬a ¬b c =  def-subst lemma1 (sym lemma0) diso where
+             lemma0 : X ≡ Ord (od→ord X)
+             lemma0 = sym Ord-ord-≡
+             lemma : osuc (od→ord z) o< od→ord X
+             lemma = ordtrans c ( c<→o< ( proj1 xx ) )
+             lemma1 : Ord ( od→ord X) ∋ ord→od (osuc (od→ord z) )
+             lemma1 = o<-subst lemma (sym diso) refl
          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 = lemma ; proj2 = <-osuc } where
-             lemma : X ∋ union-u {X} {z} X∋z
-             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} {!!} refl ord-Ord
+         union← X z UX∋z = record { proj1 = lemma ; proj2 = <-osuc } where
+             lemma : X ∋ union-u {X} {z} UX∋z
+             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl ord-Ord
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
@@ -508,7 +510,7 @@
               lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 
               lemma {y} = let open ≡-Reasoning in begin
                    def (Union (x , (x , x))) y  
-                ≡⟨ {!!} ⟩
+                ≡⟨⟩
                    def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) ))) ( osuc y )
                 ≡⟨⟩
                    osuc y o<  omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) )