Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 235:846e0926bb89
fix cardinal
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 15 Aug 2019 04:51:24 +0900 |
parents | e06b76e5b682 |
children | d09437fcfc7c |
line wrap: on
line diff
--- a/OD.agda Tue Aug 13 22:21:10 2019 +0900 +++ b/OD.agda Thu Aug 15 04:51:24 2019 +0900 @@ -490,7 +490,7 @@ ψ : ( ox : Ordinal ) → Set (suc n) ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where + lemma-ord ox = TransFinite {ψ} induction ox where ∋-p : (A x : OD ) → Dec ( A ∋ x ) ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) ∋-p A x | case1 (lift t) = yes t @@ -530,4 +530,3 @@ Select = ZF.Select OD→ZF Replace = ZF.Replace OD→ZF isZF = ZF.isZF OD→ZF -TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)