# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559151118 -32400
# Node ID c69657d0055709a39aa5344a6f4684bc975f5aaa
# Parent  94c796aee31903fc6cfb1c6346b27f7dc7d3418a
Union

diff -r 94c796aee319 -r c69657d00557 ordinal-definable.agda
--- a/ordinal-definable.agda	Thu May 30 01:56:12 2019 +0900
+++ b/ordinal-definable.agda	Thu May 30 02:31:58 2019 +0900
@@ -106,8 +106,8 @@
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-transitive : {n : Level } { x y z : OD {n} } → y ∋ x → z ∋ y → z ∋ x
-transitive  {n} {x} {y} {z} x∋y  z∋y with  ordtrans ( c<→o< {n} {x} {y} x∋y ) (  c<→o< {n} {y} {z} z∋y ) 
+transitive : {n : Level } { z y x : OD {n} } → z ∋ y → y ∋ x → z  ∋ x
+transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {n} {x} {y} x∋y ) (  c<→o< {n} {y} {z} z∋y ) 
 ... | t = lemma0 (lemma t) where
    lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
    lemma xo<z = o<→c< xo<z
@@ -349,10 +349,8 @@
          proj2 (pair A B ) =  case2 refl 
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         union→ : (X x y : OD {suc n} ) → (X ∋ x) →  (x ∋ y) →  (Union X ∋ y)
-         union→ X x y X∋x x∋y = {!!}  where
-            lemma : {z : Ordinal {suc n} } → def X z → z ≡ od→ord y
-            lemma {z} X∋z = {!!}
+         union→ :  (X x y : OD) → X ∋ x → x ∋ y → Union X ∋ y
+         union→ X x y X∋x x∋y {z} X∋z  = {!!} -- transitive {suc n} {X} {x} {y} X∋x x∋y  
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
@@ -363,7 +361,7 @@
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
-         minimul x  not = od∅
+         minimul x  not = od∅   
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = ¬∅=→∅∈ not