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

comparison constructible-set.agda @ 26:a53ba59c5bda

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