Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 28:f36e40d5d2c3
OD continue
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 May 2019 18:13:42 +0900 |
parents | bade0a35fdd9 |
children | fce60b99dc55 |
files | constructible-set.agda |
diffstat | 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 = {!!}