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

comparison OD.agda @ 291:ef93c56ad311

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 Fri, 12 Jun 2020 19:21:14 +0900
parents 359402cc6c3d 5de8905a5a2b
children be6670af87fa e70980bd80c7
comparison
equal deleted inserted replaced
290:359402cc6c3d 291:ef93c56ad311
254 ; Select = Select 254 ; Select = Select
255 ; Replace = Replace 255 ; Replace = Replace
256 ; infinite = infinite 256 ; infinite = infinite
257 ; isZF = isZF 257 ; isZF = isZF
258 } where 258 } where
259 ZFSet = OD 259 ZFSet = OD -- is less than Ords because of maxod
260 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 260 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
261 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 261 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
262 Replace : OD → (OD → OD ) → OD 262 Replace : OD → (OD → OD ) → OD
263 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x } 263 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x }
264 _∩_ : ( A B : ZFSet ) → ZFSet 264 _∩_ : ( A B : ZFSet ) → ZFSet
268 _∈_ : ( A B : ZFSet ) → Set n 268 _∈_ : ( A B : ZFSet ) → Set n
269 A ∈ B = B ∋ A 269 A ∈ B = B ∋ A
270 Power : OD → OD 270 Power : OD → OD
271 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 271 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
272 -- ｛_｝ : ZFSet → ZFSet 272 -- ｛_｝ : ZFSet → ZFSet
273 -- ｛ x ｝ = ( x , x ) 273 -- ｛ x ｝ = ( x , x ) -- it works but we don't use
274 274
275 data infinite-d : ( x : Ordinal ) → Set n where 275 data infinite-d : ( x : Ordinal ) → Set n where
276 iφ : infinite-d o∅ 276 iφ : infinite-d o∅
277 isuc : {x : Ordinal } → infinite-d x → 277 isuc : {x : Ordinal } → infinite-d x →
278 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 278 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))