# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562842830 -32400
# Node ID 3e7475fb28db823844dfe0470694f2ec3c2fd293
# Parent  53371f91ce63f564560c62cc13415f0bd3e3c288
differeent Union approach

diff -r 53371f91ce63 -r 3e7475fb28db HOD.agda
--- a/HOD.agda	Thu Jul 11 07:32:28 2019 +0900
+++ b/HOD.agda	Thu Jul 11 20:00:30 2019 +0900
@@ -262,15 +262,15 @@
  } where
     ZFSet = OD {suc n}
     Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
-    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
+    Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
     Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     _,_ : 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 } 
-    Union : OD {suc n} → OD {suc n}
-    Union U = record { def = λ y  → def U (osuc y) }
+    Union : OD {suc n} → OD {suc n}  
+    Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
@@ -325,28 +325,21 @@
 
          Union-o : (X : Ordinal {suc n}) → OD {suc n}
          Union-o X = record { def = λ y → osuc y o< X }
-         union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
-         union-ou {X} {z} U>z = Ord ( osuc ( od→ord z ) )
-         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
-         ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
-         ord-union→ x z u plt | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 plt))
-         ord-union→ x z u plt | tri< a ¬b ¬c | ()
-         ord-union→ x z u plt | tri≈ ¬a b ¬c  = subst ( λ k → k o< x ) b (proj1 plt)
-         ord-union→ x z u plt | tri> ¬a ¬b c = otrans (proj1 plt) c
-         -- ord-union← :  (x : Ordinal) (z : OD) (X∋z : Union-o x ∋ z)
-         --         → (Ord x ∋  union-ou {Ord x} {z} X∋z ) ∧ (union-ou {Ord x} {z} X∋z ∋ z )
-         -- ord-union← x z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
-         --     lemma : Ord x ∋ union-ou {Ord x} {z} X∋z
-         --     lemma = {!!} -- def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl (sym diso)
+
+--         union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
+--         union-ou {X} {z} U>z = ord→od  ( osuc ( od→ord z ) )
+--         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
+--         ord-union→ x z u plt = {!!}
+--         ord-union← :  (x : Ordinal) (z : OD) (UX∋z : Union-o x ∋ z)
+--                 → (Ord x ∋  union-ou {Ord x} {z} {!!} ) ∧ (union-ou {Ord x} {z} {!!} ∋ z )
+--         ord-union← x z UX∋z = record { proj1 = lemma ; proj2 = {!!} } where
+--             lemma : Ord x ∋ union-ou {Ord x} {z} {!!}
+--             lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
 
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = ord→od ( 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 =  def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b
-         union→ X z u xx | tri> ¬a ¬b c =  {!!}
+         union→ X z u xx = {!!}
 
          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 UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
@@ -490,7 +483,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)  )) )