### changeset 96:f239ffc27fd0

Power Set and L
author Shinji KONO Sat, 08 Jun 2019 22:17:40 +0900 f3da2c87cee0 f2b579106770 ordinal-definable.agda 1 files changed, 36 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
```--- 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}```