# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1560862875 -32400
# Node ID f91e425b341d900f006cd49676babca97daf595f
# Parent  745bee73b4441681459bc1b8c5b3500ee38dadef
dead end?

diff -r 745bee73b444 -r f91e425b341d ordinal-definable.agda
--- a/ordinal-definable.agda	Sun Jun 16 19:55:37 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 18 22:01:15 2019 +0900
@@ -84,6 +84,7 @@
 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c  with eq→ eq {y} c
 ... | t = ⊥-elim ( o<¬≡ y y refl t )
 
+
 ∅∨ : { n : Level } → { x y : Ordinal {suc n} } → ( Ord {suc n} x == Ord y ) ∨ ( ¬ ( Ord x == Ord y ) )
 ∅∨ {n} {x} {y} with trio< x y
 ∅∨ {n} {x} {y} | tri< a ¬b ¬c = case2 ( λ eq → ¬b ( ==→o≡ eq ) )
@@ -109,6 +110,8 @@
 
 -- this one cannot be proved because if we have this OD and Ordinal has one to one corespondence
 -- oc-lemma2 : { n : Level } → { x a : OD {n} } → { oa : Ordinal {n} } → oa o< od→ord (record { def = λ y → y o< oa }) → ⊥
+--   this is not allowed in our case. ( avoid one-to-one of Ord and OD )
+-- Ord=ord→od : {n : Level} →  { x : Ordinal {n} } → Ord x ≡  ord→od x
 
 _c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
@@ -198,6 +201,10 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
+O≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  Ord x == Ord y
+O≡→== {n} {x} {.x} refl = eq-refl
+
+
 >→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
 
@@ -208,6 +215,8 @@
 o<→o> {n} {x} {y} eq lt with   ==→o≡ {n} eq 
 ... | refl = o<¬≡ _ _ refl lt
 
+==-def-r : {n : Level } {x y z : Ordinal {suc n} } → (Ord x == Ord y) → def (Ord x) z → def (Ord y) z
+==-def-r {n} {x} {y} {z} eq z>x = eq→ eq z>x  
 
 o<→¬== : {n : Level} →  { x y : Ordinal {suc n} } → x o< y →  ¬ (Ord x == Ord y )
 o<→¬== {n} {x} {y} lt eq = o<→o> {n} eq lt
@@ -257,7 +266,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
 
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
-Def {n} A = record { def = λ y → y o< ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )))) }
+Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 -- Constructible Set on α
 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
@@ -266,6 +275,13 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
        record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) }
 
+Ordsuc : {n : Level} → Ordinal {suc n} → OD {suc n}
+Ordsuc x = record { def = λ y → y o< osuc x  }
+OrdSubset : {n : Level} →(A x : Ordinal {suc n} ) → OD {suc n}
+OrdSubset A x =  record { def = λ y → (y o< A) ∧ (y  o< x ) }  
+OrdDef :  {n : Level} → (A :  Ordinal {suc n}) → OD {suc n}
+OrdDef A = record { def = λ y → y o< ( sup-o ( λ x → od→ord ( OrdSubset A x))) }
+
 omega :  {n : Level} →  Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
@@ -334,19 +350,22 @@
          empty x (case1 ())
          empty x (case2 ())
 
-         power→Ord : (A t : Ordinal) → Power (Ord A) ∋ (Ord t) → {x : OD} → Ord t ∋ x → Ord A ∋ x
+         power→Ord : (A t : Ordinal) → OrdDef {suc n} A ∋ (Ord t) → {x : OD} → Ord t ∋ x → Ord A ∋ x
          power→Ord A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  OD
-              minsup =  ZFSubset (Ord A) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord A) (ord→od x))))) 
-              lemma-t : csuc minsup ∋ Ord t
-              lemma-t = ? -- o<→c< (sup-lb  P∋t)
-              lemma-s : ZFSubset (Ord A) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord A) (ord→od x)))))  ∋ x
-              lemma-s = {!!}
-         power←Ord : (A t : Ordinal) → ({x : OD} → (Ord t ∋ x → Ord A ∋ x)) → Power (Ord A) ∋ Ord t
+              minsup =  OrdSubset A ( sup-x (λ x → od→ord ( OrdSubset A x)))
+              lemma-t : Ord (sup-x (λ x → od→ord ( OrdSubset A x))) ∋ Ord t
+              lemma-t = {!!} -- sup-lb  P∋t = (od→ord (OrdSubset A (ord→od (sup-x (λ x₁ → od→ord (OrdSubset A (ord→od x₁)))))))
+              lemma-s : OrdSubset A ( sup-x (λ x → od→ord ( OrdSubset A x)))  ∋ x
+              lemma-s with osuc-≡< {suc n} ( o<-subst (c<→o< {!!} ) refl diso  )
+              lemma-s | case1 eq = {!!}
+              lemma-s | case2 lt = {!!}
+         power←Ord : (A t : Ordinal) → ({x : OD} → (Ord t ∋ x → Ord A ∋ x)) → OrdDef {suc n} A ∋ Ord t
          power←Ord = {!!}
          ---
-         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
-         --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
+         ---   ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
+         ---   Def {n} A    = record { def = λ y → y o< ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )))) }
+         ---      = Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
          --
          --  if Power A ∋ t, from a minimulity of sup, there is osuc ZFSubset A ∋ t 
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x