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

comparison cardinal.agda @ 224:afc864169325

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recover ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 10 Aug 2019 12:31:25 +0900
parents 43021d2b8756
children 5f48299929ac
comparison
equal deleted inserted replaced
223:2e1f19c949dc 224:afc864169325
1 open import Level 1 open import Level
2 module cardinal where 2 open import Ordinals
3 module cardinal {n : Level } (O : Ordinals {n}) where
3 4
4 open import zf 5 open import zf
5 open import ordinal
6 open import logic 6 open import logic
7 open import OD 7 import OD
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import Data.Nat.Properties 10 open import Data.Nat.Properties
11 open import Data.Empty 11 open import Data.Empty
12 open import Relation.Nullary 12 open import Relation.Nullary
13 open import Relation.Binary 13 open import Relation.Binary
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 15
16 open inOrdinal O
17 open OD O
16 open OD.OD 18 open OD.OD
17 19
18 open Ordinal
19 open _∧_ 20 open _∧_
20 open _∨_ 21 open _∨_
21 open Bool 22 open Bool
22 23
23 ------------ 24 ------------
25 -- Onto map 26 -- Onto map
26 -- def X x -> xmap 27 -- def X x -> xmap
27 -- X ---------------------------> Y 28 -- X ---------------------------> Y
28 -- ymap <- def Y y 29 -- ymap <- def Y y
29 -- 30 --
30 record Onto {n : Level } (X Y : OD {n}) : Set (suc n) where 31 record Onto (X Y : OD ) : Set n where
31 field 32 field
32 xmap : (x : Ordinal {n}) → def X x → Ordinal {n} 33 xmap : (x : Ordinal ) → def X x → Ordinal
33 ymap : (y : Ordinal {n}) → def Y y → Ordinal {n} 34 ymap : (y : Ordinal ) → def Y y → Ordinal
34 ymap-on-X : {y : Ordinal {n} } → (lty : def Y y ) → def X (ymap y lty) 35 ymap-on-X : {y : Ordinal } → (lty : def Y y ) → def X (ymap y lty)
35 onto-iso : {y : Ordinal {n} } → (lty : def Y y ) → xmap ( ymap y lty ) (ymap-on-X lty ) ≡ y 36 onto-iso : {y : Ordinal } → (lty : def Y y ) → xmap ( ymap y lty ) (ymap-on-X lty ) ≡ y
36 37
37 record Cardinal {n : Level } (X : OD {n}) : Set (suc n) where 38 record Cardinal (X : OD ) : Set n where
38 field 39 field
39 cardinal : Ordinal {n} 40 cardinal : Ordinal
40 conto : Onto (Ord cardinal) X 41 conto : Onto (Ord cardinal) X
41 cmax : ( y : Ordinal {n} ) → cardinal o< y → ¬ Onto (Ord y) X 42 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto (Ord y) X
42 43
43 cardinal : {n : Level } (X : OD {suc n}) → Cardinal X 44 cardinal : (X : OD ) → Cardinal X
44 cardinal {n} X = record { 45 cardinal X = record {
45 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) 46 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
46 ; conto = onto 47 ; conto = onto
47 ; cmax = cmax 48 ; cmax = cmax
48 } where 49 } where
49 cardinal-p : (x : Ordinal {suc n}) → ( Ordinal {suc n} ∧ Dec (Onto (Ord x) X) ) 50 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) )
50 cardinal-p x with p∨¬p ( Onto (Ord x) X ) 51 cardinal-p x with p∨¬p ( Onto (Ord x) X )
51 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } 52 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
52 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } 53 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
53 onto-set : OD {suc n} 54 onto-set : OD
54 onto-set = record { def = λ x → {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X } 55 onto-set = record { def = λ x → {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X }
55 onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X 56 onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
56 onto = record { 57 onto = record {
57 xmap = xmap 58 xmap = xmap
58 ; ymap = ymap 59 ; ymap = ymap
61 } where 62 } where
62 -- 63 --
63 -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one 64 -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one
64 -- od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X 65 -- od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X
65 Y = (Ord (sup-o (λ x → proj1 (cardinal-p x)))) 66 Y = (Ord (sup-o (λ x → proj1 (cardinal-p x))))
66 lemma1 : (y : Ordinal {suc n}) → def Y y → Onto (Ord y) X 67 lemma1 : (y : Ordinal ) → def Y y → Onto (Ord y) X
67 lemma1 y y<Y with sup-o< {suc n} {λ x → proj1 ( cardinal-p x)} {y} 68 lemma1 y y<Y with sup-o< {λ x → proj1 ( cardinal-p x)} {y}
68 ... | t = {!!} 69 ... | t = {!!}
69 lemma2 : def Y (od→ord X) 70 lemma2 : def Y (od→ord X)
70 lemma2 = {!!} 71 lemma2 = {!!}
71 xmap : (x : Ordinal {suc n}) → def Y x → Ordinal {suc n} 72 xmap : (x : Ordinal ) → def Y x → Ordinal
72 xmap = {!!} 73 xmap = {!!}
73 ymap : (y : Ordinal {suc n}) → def X y → Ordinal {suc n} 74 ymap : (y : Ordinal ) → def X y → Ordinal
74 ymap = {!!} 75 ymap = {!!}
75 ymap-on-X : {y : Ordinal {suc n} } → (lty : def X y ) → def Y (ymap y lty) 76 ymap-on-X : {y : Ordinal } → (lty : def X y ) → def Y (ymap y lty)
76 ymap-on-X = {!!} 77 ymap-on-X = {!!}
77 onto-iso : {y : Ordinal {suc n} } → (lty : def X y ) → xmap (ymap y lty) (ymap-on-X lty ) ≡ y 78 onto-iso : {y : Ordinal } → (lty : def X y ) → xmap (ymap y lty) (ymap-on-X lty ) ≡ y
78 onto-iso = {!!} 79 onto-iso = {!!}
79 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X 80 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
80 cmax y lt ontoy = o<> lt (o<-subst {suc n} {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))} 81 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
81 (sup-o< {suc n} {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where 82 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where
82 lemma : proj1 (cardinal-p y) ≡ y 83 lemma : proj1 (cardinal-p y) ≡ y
83 lemma with p∨¬p ( Onto (Ord y) X ) 84 lemma with p∨¬p ( Onto (Ord y) X )
84 lemma | case1 x = refl 85 lemma | case1 x = refl
85 lemma | case2 not = ⊥-elim ( not ontoy ) 86 lemma | case2 not = ⊥-elim ( not ontoy )
86 87
87 func : {n : Level} → (f : Ordinal {suc n} → Ordinal {suc n}) → OD {suc n} 88 func : (f : Ordinal → Ordinal ) → OD
88 func {n} f = record { def = λ y → (x : Ordinal {suc n}) → y ≡ f x } 89 func f = record { def = λ y → (x : Ordinal ) → y ≡ f x }
89 90
90 Func : {n : Level} → OD {suc n} 91 Func : OD
91 Func {n} = record { def = λ x → (f : Ordinal {suc n} → Ordinal {suc n}) → x ≡ od→ord (func f) } 92 Func = record { def = λ x → (f : Ordinal → Ordinal ) → x ≡ od→ord (func f) }
92 93
93 odmap : {n : Level} → { x : OD {suc n} } → Func ∋ x → Ordinal {suc n} → OD {suc n} 94 odmap : { x : OD } → Func ∋ x → Ordinal → OD
94 odmap {n} {f} lt x = record { def = λ y → def f y } 95 odmap {f} lt x = record { def = λ y → def f y }
95 96
96 lemma1 : {n : Level} → { x : OD {suc n} } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal {suc n} → Ordinal {suc n}) → ¬ ( x ≡ od→ord (func f) )) 97 lemma1 : { x : OD } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal → Ordinal ) → ¬ ( x ≡ od→ord (func f) ))
97 lemma1 = {!!} 98 lemma1 = {!!}
98 99
99 100
100 ----- 101 -----
101 -- All cardinal is ℵ0, since we are working on Countable Ordinal, 102 -- All cardinal is ℵ0, since we are working on Countable Ordinal,