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

comparison OD.agda @ 287:5de8905a5a2b

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 Sun, 07 Jun 2020 20:29:12 +0900
parents d9d3654baee1
children ef93c56ad311
comparison
equal deleted inserted replaced
286:4ae48eed654a 287:5de8905a5a2b
244 ; Select = Select 244 ; Select = Select
245 ; Replace = Replace 245 ; Replace = Replace
246 ; infinite = infinite 246 ; infinite = infinite
247 ; isZF = isZF 247 ; isZF = isZF
248 } where 248 } where
249 ZFSet = OD 249 ZFSet = OD -- is less than Ords because of maxod
250 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 250 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
251 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 251 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
252 Replace : OD → (OD → OD ) → OD 252 Replace : OD → (OD → OD ) → OD
253 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x } 253 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x }
254 _∩_ : ( A B : ZFSet ) → ZFSet 254 _∩_ : ( A B : ZFSet ) → ZFSet
258 _∈_ : ( A B : ZFSet ) → Set n 258 _∈_ : ( A B : ZFSet ) → Set n
259 A ∈ B = B ∋ A 259 A ∈ B = B ∋ A
260 Power : OD → OD 260 Power : OD → OD
261 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 261 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
262 -- ｛_｝ : ZFSet → ZFSet 262 -- ｛_｝ : ZFSet → ZFSet
263 -- ｛ x ｝ = ( x , x ) 263 -- ｛ x ｝ = ( x , x ) -- it works but we don't use
264 264
265 data infinite-d : ( x : Ordinal ) → Set n where 265 data infinite-d : ( x : Ordinal ) → Set n where
266 iφ : infinite-d o∅ 266 iφ : infinite-d o∅
267 isuc : {x : Ordinal } → infinite-d x → 267 isuc : {x : Ordinal } → infinite-d x →
268 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 268 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))