Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison cardinal.agda @ 225:5f48299929ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
224:afc864169325 225:5f48299929ac
18 open OD.OD 18 open OD.OD
19 19
20 open _∧_ 20 open _∧_
21 open _∨_ 21 open _∨_
22 open Bool 22 open Bool
23
24
25 func : (f : Ordinal → Ordinal ) → ( dom cod : OD ) → OD
26 func f dom cod = record { def = λ z → {x y : Ordinal} → (z ≡ omax x y ) ∧ def dom x ∧ def cod (f x ) }
27
28 -- Func : ( dom cod : OD ) → OD
29 -- Func dom cod = record { def = λ x → x o< sup-o ( λ y → (f : Ordinal → Ordinal ) → y ≡ od→ord (func f dom cod) ) }
23 30
24 ------------ 31 ------------
25 -- 32 --
26 -- Onto map 33 -- Onto map
27 -- def X x -> xmap 34 -- def X x -> xmap
42 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto (Ord y) X 49 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto (Ord y) X
43 50
44 cardinal : (X : OD ) → Cardinal X 51 cardinal : (X : OD ) → Cardinal X
45 cardinal X = record { 52 cardinal X = record {
46 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) 53 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
47 ; conto = onto 54 ; conto = x∋minimul onto-set ∃-onto-set
48 ; cmax = cmax 55 ; cmax = cmax
49 } where 56 } where
50 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) ) 57 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) )
51 cardinal-p x with p∨¬p ( Onto (Ord x) X ) 58 cardinal-p x with p∨¬p ( Onto (Ord x) X )
52 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } 59 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
53 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } 60 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
54 onto-set : OD 61 onto-set : OD
55 onto-set = record { def = λ x → {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X } 62 onto-set = record { def = λ x → Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X }
56 onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X 63 ∃-onto-set : ¬ ( onto-set == od∅ )
57 onto = record { 64 ∃-onto-set record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {_} ( eq→ lemma ) where
58 xmap = xmap 65 lemma : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
59 ; ymap = ymap 66 lemma = {!!}
60 ; ymap-on-X = ymap-on-X
61 ; onto-iso = onto-iso
62 } where
63 --
64 -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one
65 -- od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X
66 Y = (Ord (sup-o (λ x → proj1 (cardinal-p x))))
67 lemma1 : (y : Ordinal ) → def Y y → Onto (Ord y) X
68 lemma1 y y<Y with sup-o< {λ x → proj1 ( cardinal-p x)} {y}
69 ... | t = {!!}
70 lemma2 : def Y (od→ord X)
71 lemma2 = {!!}
72 xmap : (x : Ordinal ) → def Y x → Ordinal
73 xmap = {!!}
74 ymap : (y : Ordinal ) → def X y → Ordinal
75 ymap = {!!}
76 ymap-on-X : {y : Ordinal } → (lty : def X y ) → def Y (ymap y lty)
77 ymap-on-X = {!!}
78 onto-iso : {y : Ordinal } → (lty : def X y ) → xmap (ymap y lty) (ymap-on-X lty ) ≡ y
79 onto-iso = {!!}
80 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X 67 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
81 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))} 68 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
82 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where 69 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where
83 lemma : proj1 (cardinal-p y) ≡ y 70 lemma : proj1 (cardinal-p y) ≡ y
84 lemma with p∨¬p ( Onto (Ord y) X ) 71 lemma with p∨¬p ( Onto (Ord y) X )
85 lemma | case1 x = refl 72 lemma | case1 x = refl
86 lemma | case2 not = ⊥-elim ( not ontoy ) 73 lemma | case2 not = ⊥-elim ( not ontoy )
87 74
88 func : (f : Ordinal → Ordinal ) → OD
89 func f = record { def = λ y → (x : Ordinal ) → y ≡ f x }
90
91 Func : OD
92 Func = record { def = λ x → (f : Ordinal → Ordinal ) → x ≡ od→ord (func f) }
93
94 odmap : { x : OD } → Func ∋ x → Ordinal → OD
95 odmap {f} lt x = record { def = λ y → def f y }
96
97 lemma1 : { x : OD } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal → Ordinal ) → ¬ ( x ≡ od→ord (func f) ))
98 lemma1 = {!!}
99
100
101 -----
102 -- All cardinal is ℵ0, since we are working on Countable Ordinal, 75 -- All cardinal is ℵ0, since we are working on Countable Ordinal,
103 -- Power ω is larger than ℵ0, so it has no cardinal. 76 -- Power ω is larger than ℵ0, so it has no cardinal.
104 77
105 78
106 79