# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559999860 -32400
# Node ID f239ffc27fd01cf83e80cf26377758fe11174155
# Parent  f3da2c87cee0ed429ad90d55d7409d284403de55
Power Set and L

diff -r f3da2c87cee0 -r f239ffc27fd0 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jun 08 17:33:09 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 08 22:17:40 2019 +0900
@@ -45,6 +45,7 @@
 od∅ : {n : Level} → OD {n} 
 od∅ {n} = record { def = λ _ → Lift n ⊥ }
 
+-- OD can be iso to a subset of Ordinal
 postulate      
   od→ord : {n : Level} → OD {n} → Ordinal {n}
   ord→od : {n : Level} → Ordinal {n} → OD {n} 
@@ -247,9 +248,36 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
+-- Power Set of X ( or constructible by λ y → def X (od→ord y )
 Def :  {n : Level} →  OD {suc n} → OD {suc n}
-Def {n} X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
+Def {n} A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  → def A x }
+
+-- Constructible Set on α
+L : {n : Level} →  Ordinal {suc n} → OD {suc n}
+L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
+L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L ( record { lv = lx ; ord = ox } ))
+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 }) )) }
+
+csuc :  {n : Level} →  OD {suc n} → OD {suc n}
+csuc x = ord→od ( osuc ( od→ord x ))
 
+-- L∋ord : {n : Level} → (x :  Ordinal {suc n} ) → L (osuc x) ∋ ord→od x
+-- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!}
+-- L∋ord {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!}
+-- L∋ord {n} record { lv = lv ; ord = (OSuc .(lv) ord₁) } = {!!}
+
+--  X ⊆ OD → (P X ∩ OD ) ⊆ L (supP X) ∈  OD
+
+ord-of : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n} → Ordinal {suc n}
+ord-of {n} A x with def A x
+... | t = x
+
+supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n}
+supP A = sup-o ( ord-of A )
+
+L→P : {n : Level} → (A : OD {suc n} ) → L (supP A) ∋ Def A 
+L→P {n} A = {!!}
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
@@ -275,18 +303,18 @@
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
     Power : OD {suc n} → OD {suc n}
-    Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def (ord→od y) x  → def X x }
+    Power A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  → def A x }
     ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
-    _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
-    _∪_ : ( A B : ZFSet  ) → ZFSet
-    A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
+    -- _∩_ : ( A B : ZFSet  ) → ZFSet
+    -- A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
+    -- _∪_ : ( A B : ZFSet  ) → ZFSet
+    -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     infixr  200 _∈_
-    infixr  230 _∩_ _∪_
+    -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
     isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
     isZF = record {
@@ -315,7 +343,7 @@
          empty x ()
          --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  →  def X x }
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = {!!}
+         power→ A t P∋t {x} t∋x = P∋t (od→ord x) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x )
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A z _ = {!!}
          union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}