Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 291:ef93c56ad311
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 12 Jun 2020 19:21:14 +0900 |
parents | 359402cc6c3d 5de8905a5a2b |
children | be6670af87fa e70980bd80c7 |
line wrap: on
line diff
--- a/OD.agda Fri Jun 12 19:19:16 2020 +0900 +++ b/OD.agda Fri Jun 12 19:21:14 2020 +0900 @@ -256,7 +256,7 @@ ; infinite = infinite ; isZF = isZF } where - ZFSet = OD + ZFSet = OD -- is less than Ords because of maxod Select : (X : OD ) → ((x : OD ) → Set n ) → OD Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD → (OD → OD ) → OD @@ -270,7 +270,7 @@ Power : OD → OD Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) -- {_} : ZFSet → ZFSet - -- { x } = ( x , x ) + -- { x } = ( x , x ) -- it works but we don't use data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅