# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562709120 -32400
# Node ID f1801c4735d3a99df92cda8e98c48291fc6069cc
# Parent  996a67042f50564e42dd8d09a95b5d4e84db9262
union continue ...

diff -r 996a67042f50 -r f1801c4735d3 HOD.agda
--- a/HOD.agda	Tue Jul 09 17:46:45 2019 +0900
+++ b/HOD.agda	Wed Jul 10 06:52:00 2019 +0900
@@ -318,6 +318,17 @@
          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 ) )
+         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union (Ord 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
+             lemma : Ord x ∋ union-u {Ord x} {z} X∋z
+             lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl ?
+
          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))