# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562727026 -32400
# Node ID e51c23eb3803993ad10c68a366fd96038779563f
# Parent  f1801c4735d3a99df92cda8e98c48291fc6069cc
union trying ..

diff -r f1801c4735d3 -r e51c23eb3803 HOD.agda
--- a/HOD.agda	Wed Jul 10 06:52:00 2019 +0900
+++ b/HOD.agda	Wed Jul 10 11:50:26 2019 +0900
@@ -214,7 +214,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
 
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
-Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
+Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→
 
 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
 OrdSubset {n} A x = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
@@ -313,38 +313,39 @@
 
          ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x}
          ord-⊆ t x lt = c<→o< lt
+         o<→c< :  {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_  (Ord x) (Ord y) {z}
+         o<→c< lt lt1 = ordtrans lt1 lt 
+         --   a ⊆ b → od→ord a o≤ od→ord b ?   
 
-         union-d : (X : OD {suc n}) → OD {suc n}
-         union-d X = record { def = λ y → def X (osuc y) }
+         Union-o : (X : Ordinal {suc n}) → OD {suc n}
+         Union-o X = record { def = λ y → osuc y o< X }
+
          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 ) )
-         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union (Ord x) ∋ z
+         union-u {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 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 (Ord x) ∋ z) → (Ord x ∋  union-u {Ord x} {z} X∋z ) ∧ (union-u {Ord x} {z} X∋z ∋ z )
-         ord-union← x z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
+         ord-union← :  (x : Ordinal) (z : OD) (X∋z : Union-o x ∋ z)
+                 → (Ord x ∋  union-u {Ord x} {z} X∋z ) ∧ (union-u {Ord x} {z} X∋z ∋ z )
+         ord-union← x z X∋z = record { proj1 = lemma ; proj2 = {!!} } where
              lemma : Ord x ∋ union-u {Ord x} {z} X∋z
-             lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl ?
+             lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl (sym diso)
 
          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 =  def-subst lemma1 (sym lemma0) diso where
-             lemma0 : X ≡ Ord (od→ord X)
-             lemma0 = sym {!!}
-             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 u xx | tri> ¬a ¬b c =  {!!}
          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 = <-osuc } where
+         union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } 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 {!!}
+             lemma = {!!} -- def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!}
+             lemma2 : union-u {X} UX∋z ∋ z
+             lemma2 = {!!}
 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t