Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison constructible-set.agda @ 25:0f3d98e97593

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 May 2019 16:28:10 +0900
parents 3186bbee99dd
children a53ba59c5bda
comparison
equal deleted inserted replaced
24:3186bbee99dd 25:0f3d98e97593
180 a ∋ x = ( α x o< α a ) ∧ constructible a ( α x ) 180 a ∋ x = ( α x o< α a ) ∧ constructible a ( α x )
181 181
182 c∅ : {n : Level} → ConstructibleSet 182 c∅ : {n : Level} → ConstructibleSet
183 c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ } 183 c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ }
184 184
185 record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m ) (ψ : S → S ) (X : S) : Set (n ⊔ m) where 185 record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m ) (ψ : S → S ) (X : S) : Set ((suc n) ⊔ m) where
186 field 186 field
187 sup : S 187 sup : S
188 smax : ∀ { x : S } → x ≤ X → ψ x ≤ sup 188 smax : ∀ { x : S } → x ≤ X → ψ x ≤ sup
189 suniq : {max : S} → ( ∀ { x : S } → x ≤ X → ψ x ≤ max ) → max ≤ sup 189 suniq : {max : S} → ( ∀ { x : S } → x ≤ X → ψ x ≤ max ) → max ≤ sup
190 repl : ( x : Ordinal {n} ) → Set n
190 191
191 open SupR 192 open SupR
192 193
193 _⊆_ : {n : Level} → ( A B : ConstructibleSet ) → ∀{ x : ConstructibleSet } → Set (suc n) 194 _⊆_ : {n : Level} → ( A B : ConstructibleSet ) → ∀{ x : ConstructibleSet } → Set (suc n)
194 _⊆_ A B {x} = A ∋ x → B ∋ x 195 _⊆_ A B {x} = A ∋ x → B ∋ x
198 199
199 Sup : {n : Level } → (ψ : ConstructibleSet → ConstructibleSet ) → (X : ConstructibleSet) → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X 200 Sup : {n : Level } → (ψ : ConstructibleSet → ConstructibleSet ) → (X : ConstructibleSet) → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
200 sup (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ 201 sup (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ
201 smax (Sup ψ X ) = {!!} 202 smax (Sup ψ X ) = {!!}
202 suniq (Sup ψ X ) = {!!} 203 suniq (Sup ψ X ) = {!!}
204 repl (Sup ψ X ) = {!!}
203 205
204 open import Data.Unit 206 open import Data.Unit
205 open SupR 207 open SupR
206 208
207 ConstructibleSet→ZF : {n : Level} → ZF {suc n} {suc n} 209 ConstructibleSet→ZF : {n : Level} → ZF {suc n} {suc n}
212 ; ∅ = c∅ 214 ; ∅ = c∅
213 ; _,_ = _,_ 215 ; _,_ = _,_
214 ; Union = Union 216 ; Union = Union
215 ; Power = {!!} 217 ; Power = {!!}
216 ; Select = Select 218 ; Select = Select
217 ; Replace = {!!} 219 ; Replace = Replace
218 ; infinite = {!!} 220 ; infinite = {!!}
219 ; isZF = {!!} 221 ; isZF = {!!}
220 } where 222 } where
221 conv : {n : Level} → (ConstructibleSet {n} → Set (suc (suc n))) → ConstructibleSet → Set (suc n)
222 conv {n} ψ x with ψ x
223 ... | t = Lift ( suc n ) ⊤
224 Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n} 223 Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n}
225 Select X ψ = record { α = α X ; constructible = λ x → {!!} } -- ψ (record { α = x ; constructible = λ x → constructible X x } ) } 224 Select X ψ = record { α = α X ; constructible = λ x → select x } where
225 select : Ordinal → Set n
226 select x with ψ (record { α = x ; constructible = λ x → constructible X x })
227 ... | t = Lift n ⊤
226 Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet 228 Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
227 Replace X ψ = record { α = α (sup supψ) ; constructible = λ x → {!!} } where 229 Replace X ψ = record { α = α (sup supψ) ; constructible = λ x → repl1 x } where
228 supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X 230 supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
229 supψ = Sup ψ X 231 supψ = Sup ψ X
230 repl : Ordinal {n} → Set (suc n) 232 repl1 : Ordinal {suc n} → Set n
231 repl x = {!!} 233 repl1 x with repl supψ x
232 conv1 : (Ordinal {n} → Set n) → Ordinal {n} → Set n 234 ... | t = Lift n ⊤
233 conv1 ψ x with ψ
234 ... | t = Lift n ⊤
235 _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet 235 _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
236 a , b = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} } -- ((x ≡ α a ) ∨ ( x ≡ α b )) } 236 a , b = record { α = maxα (α a) (α b) ; constructible = a∨b } where
237 a∨b : Ordinal {suc n} → Set n
238 a∨b x with (x ≡ α a ) ∨ ( x ≡ α b )
239 ... | t = Lift n ⊤
237 Union : ConstructibleSet → ConstructibleSet 240 Union : ConstructibleSet → ConstructibleSet
238 Union a = {!!} 241 Union a = {!!}