Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 217:d5668179ee69
cardinal continue
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Aug 2019 17:02:37 +0900 |
| parents | 5b9b6ef971dd |
| children | eee983e4b402 |
| files | OD.agda |
| diffstat | 1 files changed, 34 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Sun Aug 04 18:09:00 2019 +0900 +++ b/OD.agda Mon Aug 05 17:02:37 2019 +0900 @@ -646,11 +646,39 @@ cardinal : {n : Level } (X : OD {suc n}) → Cardinal X cardinal {n} X = record { - cardinal = sup-o ( λ x → cardinal-p x ) - ; conto = {!!} - ; cmax = {!!} + cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) + ; conto = onto + ; cmax = cmax } where - cardinal-p : (x : Ordinal {suc n}) → Ordinal {suc n} + cardinal-p : (x : Ordinal {suc n}) → ( Ordinal {suc n} ∧ Dec (Onto (Ord x) X) ) cardinal-p x with p∨¬p ( Onto (Ord x) X ) - cardinal-p x | case1 True = x - cardinal-p x | case2 False = o∅ + cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } + cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } + onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X + onto = record { + xmap = xmap + ; ymap = ymap + ; xmap-on-Y = xmap-on-Y + ; ymap-on-X = ymap-on-X + ; onto-iso = onto-iso + } where + Y = (Ord (sup-o (λ x → proj1 (cardinal-p x)))) + xmap : (x : Ordinal {suc n}) → Ordinal {suc n} + xmap = {!!} + ymap : (y : Ordinal {suc n}) → Ordinal {suc n} + ymap = {!!} + xmap-on-Y : (x : Ordinal {suc n} ) → def Y x → def X (xmap x) + xmap-on-Y = {!!} + ymap-on-X : (y : Ordinal {suc n} ) → def X y → def Y (ymap y) + ymap-on-X = {!!} + onto-iso : (y : Ordinal {suc n} ) → def X y → xmap ( ymap y ) ≡ y + onto-iso = {!!} + cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X + cmax y lt ontoy = o<> lt (o<-subst {suc n} {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))} + (sup-o< {suc n} {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where + lemma : proj1 (cardinal-p y) ≡ y + lemma with p∨¬p ( Onto (Ord y) X ) + lemma | case1 x = refl + lemma | case2 not = ⊥-elim ( not ontoy ) + +