Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff cardinal.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 | 650bdad56729 |
line wrap: on
line diff
--- a/cardinal.agda Tue Aug 13 22:21:10 2019 +0900 +++ b/cardinal.agda Thu Aug 15 04:51:24 2019 +0900 @@ -55,9 +55,8 @@ func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where - lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt lemma : Ordinal → Ordinal - lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y) + lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) lemma y | p | no n = o∅ lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) ... | t with decp ( x ≡ π1 t ) @@ -71,10 +70,10 @@ -- contra position of sup-o< -- -postulate - -- contra-position of mimimulity of supermum required in Cardinal - sup-x : ( Ordinal → Ordinal ) → Ordinal - sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) +-- postulate +-- -- contra-position of mimimulity of supermum required in Cardinal +-- sup-x : ( Ordinal → Ordinal ) → Ordinal +-- sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) ------------ --