# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561446271 -32400
# Node ID 5f97ebaeb89ba88f49fcbb63d4f07ae3d1e9b266
# Parent  c42352a7ee077ee8bc81a4d88541e4af15664b78
...

diff -r c42352a7ee07 -r 5f97ebaeb89b HOD.agda
--- a/HOD.agda	Tue Jun 25 05:50:22 2019 +0900
+++ b/HOD.agda	Tue Jun 25 16:04:31 2019 +0900
@@ -54,17 +54,16 @@
 od∅ : {n : Level} → HOD {n} 
 od∅ {n} = Ord o∅ 
 
-data SinO {n : Level} : (ox : Ordinal {n}) (x : HOD {n}) → Set (suc n) where
-  o-in-o : {ox : Ordinal {n} } → SinO ox (Ord ox)
-  s-in-o : {ox : Ordinal {n} } → {y x : HOD {n} } → SinO ox y → x == y → SinO ox x
-
 postulate      
   -- HOD can be iso to a subset of Ordinal ( by means of Godel Set )
   od→ord : {n : Level} → HOD {n} → Ordinal {n}
+  ord→od : {n : Level} → Ordinal {n} → HOD {n} 
+  oiso   : {n : Level} {x : HOD {n}}     → ord→od ( od→ord x ) ≡ x
+  diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
+  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   -- necessary?
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
-  sino   : {n : Level} {x : HOD {n}}     → SinO ( od→ord x ) x
   -- supermum as Replacement Axiom
   sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-o< : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
@@ -73,31 +72,26 @@
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
 
-
 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
 _c<_ : { n : Level } → ( x a : HOD {n} ) → Set n
 x c< a = a ∋ x 
 
-postulate      
-  o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y  → Ord y ∋ Ord x 
-
-ord→od : {n : Level} → Ordinal {n} → HOD {n} 
-ord→od = ?
-
-oiso   : {n : Level} {x : HOD {n}} → ? ≡ x
-oiso   = ?
-
-diso   : {n : Level} {x : Ordinal {n}} → od→ord ? ≡ x
-diso   = ?
-
 _c≤_ : {n : Level} →  HOD {n} →  HOD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
+cseq : {n : Level} →  HOD {n} →  HOD {n}
+cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where
+   lemma : {ox oy : Ordinal} → osuc ox o< od→ord x → oy o< ox → osuc oy o< od→ord x
+   lemma {ox} {oy} oox<Ox oy<ox  = ordtrans (osucc oy<ox ) oox<Ox 
+
 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
+o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 
+o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt 
+
 sup-od : {n : Level } → ( HOD {n} → HOD {n}) →  HOD {n}
 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
 
@@ -179,20 +173,11 @@
 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
     lemma :  o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
-    lemma lt with def-subst {!!} oiso refl
-    lemma lt | t = {!!}
+    lemma lt with o<→c< lt 
+    lemma lt | t = o<¬≡ refl t
 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
-ord-od∅ :  {n : Level} → o∅ {suc n} ≡ od→ord (Ord (o∅ {suc n}))
-ord-od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (Ord (o∅ {suc n})))
-ord-od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
-    lemma :  o∅ {suc n } o< (od→ord (Ord (o∅ {suc n}))) → ⊥
-    lemma lt with  o<→c< lt
-    lemma lt | t = o<¬≡ refl t
-ord-od∅ {n} | tri≈ ¬a b ¬c = b
-ord-od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-
 o<→¬c> : {n : Level} →  { x y : HOD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 
@@ -262,14 +247,21 @@
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = sup-od ψ
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → X ∋ x → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x →  ( (d : def X x ) →  ψ (ord→od x) (subst (λ k → def X k ) (sym diso) d)) ; otrans = lemma }  where
-       lemma : {x y : Ordinal} → ((d : def X x) → ψ (ord→od x) (subst (def X) (sym diso) d)) →
-            y o< x → (d : def X y) → ψ (ord→od y) (subst (def X) (sym diso) d)
-       lemma {x} {y} f y<x d = {!!}
+    Select X ψ = record { def = λ x → (d : def X x ) → f x d ; otrans = ftrans }  where
+       f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n) 
+       f x d = ψ (ord→od x)  (subst (λ k → def X k ) (sym diso) d)
+       ftrans : {x y : Ordinal} → ((d : def X x) → f x d) → y o< x → (d : def X y) → f y d
+       ftrans {x} {y} g  = TransFinite {suc n} {λ y1 → (y1<x : y1 o< x)  → (d1 : def X y1)  → f y1 d1} lemma1 lemma2 y where
+          lemma1 :  (lx : Nat) → record { lv = lx ; ord = Φ lx } o< x → (d1 : def X (record { lv = lx ; ord = Φ lx })) → f (record { lv = lx ; ord = Φ lx }) d1
+          lemma1 = {!!}
+          lemma2 : (lx : Nat) (x₁ : OrdinalD lx) → (record { lv = lx ; ord = x₁ } o< x →
+             (d1 : def X (record { lv = lx ; ord = x₁ })) → f (record { lv = lx ; ord = x₁ }) d1) → record { lv = lx ; ord = OSuc lx x₁ } o< x →
+             (d1 : def X (record { lv = lx ; ord = OSuc lx x₁ })) → f (record { lv = lx ; ord = OSuc lx x₁ }) d1
+          lemma2 = {!!}
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}
-    Union U = record { def = λ y → osuc y o< (od→ord U) ; otrans = {!!} }
+    Union U = cseq U 
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
     Power : HOD {suc n} → HOD {suc n}
     Power A = Def A
diff -r c42352a7ee07 -r 5f97ebaeb89b ordinal.agda
--- a/ordinal.agda	Tue Jun 25 05:50:22 2019 +0900
+++ b/ordinal.agda	Tue Jun 25 16:04:31 2019 +0900
@@ -97,6 +97,11 @@
 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
 osuc-lveq {n} = refl
 
+osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox  → osuc oy o< osuc ox
+osucc {n} {ox} {oy} (case1 x) = case1 x
+osucc {n} {ox} {oy} (case2 x) with d<→lv x
+... | refl = case2 (s< x)
+
 nat-<> : { x y : Nat } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x