# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559352233 -32400
# Node ID d088eb66564e411eb0ea40d7a3e865d22d34f4fc
# Parent  cd9cf8b096102e97cb60e114ca3d5746115912f4
add osuc ( next larger element of Ordinal )

diff -r cd9cf8b09610 -r d088eb66564e ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jun 01 10:01:38 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 10:23:53 2019 +0900
@@ -312,7 +312,7 @@
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {suc n} → OD {suc n}
-    Union U = record { def = λ y → y o< (od→ord U) }
+    Union U = record { def = λ y → osuc y o< (od→ord U) }
     Power : OD {suc n} → OD {suc n}
     Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y )  }
     ZFSet = OD {suc n}
@@ -353,26 +353,17 @@
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
          union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
-         union-u X z U>z with od→ord X | od→ord z 
-         union-u X z (case1 (s≤s x)) | record { lv = Suc lX ; ord = oX } | record { lv = lz ; ord = oz } = ord→od (mid (Suc lX) lz oX oz (s≤s x) )  where
-             mid : (lX lz : Nat) → (oX : OrdinalD {suc n} lX ) → (oz : OrdinalD {suc n} lz ) → lX > lz  → Ordinal {suc n}
-             mid (Suc lX) 0 oX oz (s≤s z≤n) = record { lv = 0 ; ord = OSuc 0 oz }
-             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (Φ (Suc lz)) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (Φ (Suc lz) ) }
-             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (OSuc (Suc lz) oz) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (OSuc (Suc lz) oz) }
-             mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (ℵ lz) (s≤s (s≤s lt)) = record { lv = (Suc (Suc lX)) ; ord = OSuc (Suc (Suc lX)) (ℵ (Suc lX)) }
-             mid (Suc (Suc lX)) (Suc lz) (OSuc (Suc (Suc lX)) oX) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = oX }
-             mid (Suc (Suc lX)) (Suc lz) (ℵ (Suc lX)) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = OSuc (Suc (Suc lX)) (Φ (Suc (Suc lX))) }
-         union-u X z (case2 Φ<) | record { lv = Zero ; ord = (OSuc 0 oX) } | record { lv = .0 ; ord = .(Φ 0) } =
-             ord→od (record { lv = Zero ; ord = oX }) -- this case contains X = odΦ
-         union-u X z (case2 Φ<) | record { lv = Suc lv₁ ; ord = (OSuc (Suc lv₁) oX) } | record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) } =  ord→od (record { lv = Suc lv₁ ; ord = oX } )
+         union-u X z U>z with od→ord X | osuc (od→ord z )
+         union-u X z (case1 (s≤s z≤n)) | record { lv = .(Suc _) ; ord = ord₁ } | record { lv = .0 ; ord = ord₂ } = {!!}
+         union-u X z (case1 (s≤s (s≤s x))) | record { lv = .(Suc (Suc _)) ; ord = ord₁ } | record { lv = .(Suc _) ; ord = ord₂ } = {!!}
+         union-u X z (case2 Φ<) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(Φ lv₁) } = {!!}
          union-u X z (case2 (s< x)) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(OSuc lv₁ _) } = {!!}
-         union-u X z (case2 ℵΦ<) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } =  ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (Φ (Suc lX))} )
-         union-u X z (case2 (ℵ< x)) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = OSuc (Suc _) oz } =
-              ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (OSuc (Suc lX) (OSuc (Suc lX) oz ))} )
-         union-u X z (case2 ℵs<) | record { lv = Suc lX ; ord = OSuc (Suc lX) (ℵ lX) } | record { lv = Suc lX ; ord = ℵ lX } = {!!}
+         union-u X z (case2 ℵΦ<) | record { lv = .(Suc _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } = {!!}
+         union-u X z (case2 (ℵ< x)) | record { lv = .(Suc _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } = {!!}
+         union-u X z (case2 ℵs<) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
          union-u X z (case2 (ℵss< x)) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
          union→ :  (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
-         union→ X x y X∋x x∋y =  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
+         union→ X x y X∋x x∋y = {!!} --  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
          union← :  (X z : OD {suc n}) → (X∋z : Union X ∋ z) → ((Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z))
          union← = {!!}
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
diff -r cd9cf8b09610 -r d088eb66564e ordinal.agda
--- a/ordinal.agda	Sat Jun 01 10:01:38 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 10:23:53 2019 +0900
@@ -41,6 +41,11 @@
 o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
 o<-subst df refl refl = df
 
+osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
+osuc record { lv = lx ; ord = (Φ lv) } = record { lv = lx ; ord = OSuc lx (Φ lv) }
+osuc record { lv = lx ; ord = (OSuc lx ox ) } =  record { lv = lx ; ord = OSuc lx ox }
+osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) }
+
 open import Data.Nat.Properties 
 open import Data.Empty
 open import Data.Unit using ( ⊤ )