### changeset 28:f36e40d5d2c3

OD continue
author Shinji KONO Sun, 19 May 2019 18:13:42 +0900 bade0a35fdd9 fce60b99dc55 constructible-set.agda 1 files changed, 37 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
```--- a/constructible-set.agda	Sun May 19 15:30:04 2019 +0900
+++ b/constructible-set.agda	Sun May 19 18:13:42 2019 +0900
@@ -190,8 +190,8 @@
open import Data.Unit

postulate      -- this is proved by Godel numbering of def
-   _c<_ : {n : Level } → (x y : OD {n} ) → Set n
-   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {n} _≡_ _c<_
+   _c<_ : {n : Level } → (x y : OD {n} ) → Set (suc n)
+   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {suc n} _≡_ _c<_

-- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
-- o∋ a x x<A  = def a x x<A
@@ -207,10 +207,40 @@
--
--     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
--
---    HOD = {x | TC x ⊆ OD }  ⊆ OD
+-- Heritic Ordinal Definable
+--
+--    ( HOD = {x | TC x ⊆ OD } ) ⊆ OD
--

-record HOD {n : Level}  : Set (suc n) where
-  field
-      hod : OD {n}
-      tc : ?
+HOD = OD
+
+c∅ : {n : Level} → HOD {n}
+c∅ {n} = record { α  = o∅ ; def = λ x y → Lift n ⊥ }
+
+HOD→ZF : {n : Level} → ZF {suc n} {suc n}
+HOD→ZF {n}  = record {
+    ZFSet = HOD
+    ; _∋_ = λ a b → b c< a
+    ; _≈_ = _≡_
+    ; ∅  = c∅
+    ; _,_ = _,_
+    ; Union = Union
+    ; Power = {!!}
+    ; Select = Select
+    ; Replace = Replace
+    ; infinite = {!!}
+    ; isZF = {!!}
+ } where
+    Select : (X : HOD {n}) → (HOD {n} → Set (suc n)) → HOD {n}
+    Select X ψ = record { α = α X ; def = λ x →  {!!} } where
+       select : Ordinal → Set n
+       select x with  ψ (record { α = x ; def = λ x → {!!} })
+       ... | t = Lift n ⊤
+    Replace : (X : HOD {n} ) → (HOD → HOD) → HOD
+    Replace X ψ  = record { α = {!!} ; def = λ x → {!!} }
+    _,_ : HOD {n} → HOD → HOD
+    a , b  = record { α = maxα (α a) (α b) ; def = λ x x<ab → (   ) }  where
+       a∨b : Ordinal {suc n} → Set n
+       a∨b = {!!}
+    Union : HOD → HOD
+    Union a = {!!}```