Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff constructible-set.agda @ 18:627a79e61116
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 16 May 2019 10:55:34 +0900 |
parents | 6a668c6086a5 |
children | 47995eb521d4 |
line wrap: on
line diff
--- a/constructible-set.agda Tue May 14 13:52:19 2019 +0900 +++ b/constructible-set.agda Thu May 16 10:55:34 2019 +0900 @@ -122,55 +122,37 @@ -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' -data Constructible ( α : Ordinal ) : Set (suc n) where - fsub : ( ψ : Ordinal → Set n ) → Constructible α - xself : Ordinal → Constructible α - record ConstructibleSet : Set (suc n) where field α : Ordinal - constructible : Constructible α + constructible : Ordinal → Set n open ConstructibleSet -data _c∋_ : {α α' : Ordinal } → - Constructible α → Constructible α' → Set n where - c> : {α α' : Ordinal } - (ta : Constructible α ) ( tx : Constructible α' ) → α' o< α → ta c∋ tx - xself-fsub : {α : Ordinal } - (ta : Ordinal ) ( ψ : Ordinal → Set n ) → _c∋_ {α} {α} (xself ta ) ( fsub ψ) - fsub-fsub : {α : Ordinal } - ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n ) → - ( ∀ ( x : Ordinal ) → ψ x → ψ₁ x ) → _c∋_ {α} {α} ( fsub ψ ) ( fsub ψ₁) - -_∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n -a ∋ x = constructible a c∋ constructible x +_∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n +a ∋ x = (α a ≡ α x) ∨ ( α x o< α a ) -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c -- ... | t1 | t2 = {!!} -data _c≈_ : {α α' : Ordinal} → - Constructible α → Constructible α' → Set n where - crefl : {α : Ordinal } → _c≈_ {α} {α} (xself α ) (xself α ) - feq : {lv : Nat} {α : Ordinal } - → ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n ) - → (∀ ( x : Ordinal ) → ψ x ⇔ ψ₁ x ) → _c≈_ {α} {α} ( fsub ψ ) ( fsub ψ₁) - -_≈_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n -a ≈ x = constructible a c≈ constructible x - -ConstructibleSet→ZF : ZF {suc n} +ConstructibleSet→ZF : ZF {suc n} {suc n} ConstructibleSet→ZF = record { ZFSet = ConstructibleSet - ; _∋_ = _∋_ - ; _≈_ = _≈_ - ; ∅ = record { α = record {lv = Zero ; ord = Φ } ; constructible = xself ( record {lv = Zero ; ord = Φ }) } - ; _×_ = {!!} - ; Union = {!!} + ; _∋_ = λ a b → Lift (suc n) ( a ∋ b ) + ; _≈_ = _≡_ + ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift n ⊥ } + ; _,_ = _,_ + ; Union = Union ; Power = {!!} - ; Select = {!!} + ; Select = Select ; Replace = {!!} ; infinite = {!!} ; isZF = {!!} - } + } where + Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet + Select = {!!} + _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet + a , b = Select {!!} {!!} + Union : ConstructibleSet → ConstructibleSet + Union a = {!!}