Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff cardinal.agda @ 225:5f48299929ac
does not work
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 11 Aug 2019 08:10:13 +0900 |
parents | afc864169325 |
children | 176ff97547b4 |
line wrap: on
line diff
--- a/cardinal.agda Sat Aug 10 12:31:25 2019 +0900 +++ b/cardinal.agda Sun Aug 11 08:10:13 2019 +0900 @@ -21,6 +21,13 @@ open _∨_ open Bool + +func : (f : Ordinal → Ordinal ) → ( dom cod : OD ) → OD +func f dom cod = record { def = λ z → {x y : Ordinal} → (z ≡ omax x y ) ∧ def dom x ∧ def cod (f x ) } + +-- Func : ( dom cod : OD ) → OD +-- Func dom cod = record { def = λ x → x o< sup-o ( λ y → (f : Ordinal → Ordinal ) → y ≡ od→ord (func f dom cod) ) } + ------------ -- -- Onto map @@ -44,7 +51,7 @@ cardinal : (X : OD ) → Cardinal X cardinal X = record { cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) - ; conto = onto + ; conto = x∋minimul onto-set ∃-onto-set ; cmax = cmax } where cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) ) @@ -52,31 +59,11 @@ cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } onto-set : OD - onto-set = record { def = λ x → {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X } - onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X - onto = record { - xmap = xmap - ; ymap = ymap - ; ymap-on-X = ymap-on-X - ; onto-iso = onto-iso - } where - -- - -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one - -- od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X - Y = (Ord (sup-o (λ x → proj1 (cardinal-p x)))) - lemma1 : (y : Ordinal ) → def Y y → Onto (Ord y) X - lemma1 y y<Y with sup-o< {λ x → proj1 ( cardinal-p x)} {y} - ... | t = {!!} - lemma2 : def Y (od→ord X) - lemma2 = {!!} - xmap : (x : Ordinal ) → def Y x → Ordinal - xmap = {!!} - ymap : (y : Ordinal ) → def X y → Ordinal - ymap = {!!} - ymap-on-X : {y : Ordinal } → (lty : def X y ) → def Y (ymap y lty) - ymap-on-X = {!!} - onto-iso : {y : Ordinal } → (lty : def X y ) → xmap (ymap y lty) (ymap-on-X lty ) ≡ y - onto-iso = {!!} + onto-set = record { def = λ x → Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X } + ∃-onto-set : ¬ ( onto-set == od∅ ) + ∃-onto-set record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {_} ( eq→ lemma ) where + lemma : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X + lemma = {!!} cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))} (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where @@ -85,20 +72,6 @@ lemma | case1 x = refl lemma | case2 not = ⊥-elim ( not ontoy ) -func : (f : Ordinal → Ordinal ) → OD -func f = record { def = λ y → (x : Ordinal ) → y ≡ f x } - -Func : OD -Func = record { def = λ x → (f : Ordinal → Ordinal ) → x ≡ od→ord (func f) } - -odmap : { x : OD } → Func ∋ x → Ordinal → OD -odmap {f} lt x = record { def = λ y → def f y } - -lemma1 : { x : OD } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal → Ordinal ) → ¬ ( x ≡ od→ord (func f) )) -lemma1 = {!!} - - ------ -- All cardinal is ℵ0, since we are working on Countable Ordinal, -- Power ω is larger than ℵ0, so it has no cardinal.