# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561548750 -32400
# Node ID 78fe704c3543652ece6a4d4d6f089d1a7e68ffba
# Parent  a4c97390d312cb726b27e0ae510c510d8afc12c1
Union done

diff -r a4c97390d312 -r 78fe704c3543 HOD.agda
--- a/HOD.agda	Wed Jun 26 08:38:33 2019 +0900
+++ b/HOD.agda	Wed Jun 26 20:32:30 2019 +0900
@@ -83,9 +83,9 @@
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
 cseq : {n : Level} →  HOD {n} →  HOD {n}
-cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where
-   lemma : {ox : Ordinal} → osuc ox o< od→ord x → { oy : Ordinal}→ oy o< ox → osuc oy o< od→ord x
-   lemma {ox}  oox<Ox {oy} oy<ox  = ordtrans (osucc oy<ox ) oox<Ox 
+cseq x = record { def = λ y → def x (osuc y) ; otrans = lemma } where
+   lemma : {ox : Ordinal} → def x (osuc ox) → { oy : Ordinal}→ oy o< ox → def x (osuc oy)
+   lemma {ox}  oox<Ox {oy} oy<ox  = otrans x  oox<Ox (osucc oy<ox )
 
 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -280,7 +280,7 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = λ _ z _ → csuc z
+       ;   union-u = λ X z UX∋z → union-u {X} {z} UX∋z
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
@@ -335,20 +335,18 @@
               lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
               lemma = sup-o<   
-         union-lemma-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → csuc 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} {!!} refl refl
+         union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
+         union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
          union→ :  (X z u : HOD) → (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 with  osuc-< a (c<→o< (proj2 xx))
-         union→ X y u xx | tri< a ¬b ¬c | ()
-         union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
-             lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
-             lemma refl lt = lt
-         union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
-         union← :  (X z : HOD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
-         union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u 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 = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b where
+         union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c
+         union← :  (X z : HOD) (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 )))} X∋z refl ord-Ord
          ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
@@ -384,7 +382,7 @@
              lemma : {x  : HOD {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)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
          uxxx-union : {x  : HOD {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 ; otrans = {!!} } ) lemma where
+         uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) {!!} where
              lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
              lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!}
          uxxx-2 : {x  : HOD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }