# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562797948 -32400
# Node ID 53371f91ce63f564560c62cc13415f0bd3e3c288
# Parent  e51c23eb3803993ad10c68a366fd96038779563f
union continue

diff -r e51c23eb3803 -r 53371f91ce63 HOD.agda
--- a/HOD.agda	Wed Jul 10 11:50:26 2019 +0900
+++ b/HOD.agda	Thu Jul 11 07:32:28 2019 +0900
@@ -314,32 +314,40 @@
          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 ?   
+         o<→c< lt lt1 = ordtrans lt1 lt
+         
+         ⊆→o< :  {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_  (Ord x) (Ord y) {z} ) →  x o< osuc y
+         ⊆→o< {x} {y}  lt with trio< x y 
+         ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
+         ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
+         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
+         ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
 
          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→od ( osuc ( od→ord z ) )
+         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-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 (sym diso)
+         -- 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-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 : 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
              lemma : X ∋ union-u {X} {z} UX∋z