|
1175
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2
|
|
431
|
3 open import Level
|
|
|
4 open import Ordinals
|
|
|
5 module cardinal {n : Level } (O : Ordinals {n}) where
|
|
|
6
|
|
|
7 open import zf
|
|
|
8 open import logic
|
|
1095
|
9 -- import OD
|
|
|
10 import OD hiding ( _⊆_ )
|
|
|
11
|
|
431
|
12 import ODC
|
|
|
13 import OPair
|
|
1095
|
14 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
431
|
15 open import Relation.Binary.PropositionalEquality
|
|
1095
|
16 open import Data.Nat.Properties
|
|
431
|
17 open import Data.Empty
|
|
|
18 open import Relation.Nullary
|
|
|
19 open import Relation.Binary
|
|
|
20 open import Relation.Binary.Core
|
|
|
21
|
|
|
22 open inOrdinal O
|
|
|
23 open OD O
|
|
|
24 open OD.OD
|
|
|
25 open OPair O
|
|
|
26 open ODAxiom odAxiom
|
|
|
27
|
|
|
28 import OrdUtil
|
|
|
29 import ODUtil
|
|
|
30 open Ordinals.Ordinals O
|
|
|
31 open Ordinals.IsOrdinals isOrdinal
|
|
|
32 open Ordinals.IsNext isNext
|
|
|
33 open OrdUtil O
|
|
|
34 open ODUtil O
|
|
|
35
|
|
1095
|
36 _⊆_ : ( A B : HOD ) → Set n
|
|
|
37 _⊆_ A B = {x : Ordinal } → odef A x → odef B x
|
|
|
38
|
|
431
|
39
|
|
|
40 open _∧_
|
|
|
41 open _∨_
|
|
|
42 open Bool
|
|
|
43 open _==_
|
|
|
44
|
|
|
45 open HOD
|
|
|
46
|
|
|
47 -- _⊗_ : (A B : HOD) → HOD
|
|
|
48 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
|
|
|
49
|
|
1174
|
50 record Func (A B : HOD) : Set n where
|
|
|
51 field
|
|
|
52 func : Ordinal → Ordinal
|
|
|
53 is-func : {x : Ordinal } → odef A x → odef B (func x)
|
|
|
54
|
|
|
55 data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where
|
|
|
56 felm : (F : Func A B) → FuncHOD A B (& ( Replace A ( λ x → < x , (* (Func.func F (& x))) > )))
|
|
|
57
|
|
|
58 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
|
|
|
59 FuncHOD→F {A} {B} (felm F) = F
|
|
431
|
60
|
|
1174
|
61 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
|
|
|
62 FuncHOD=R {A} {B} (felm F) = *iso
|
|
|
63
|
|
1175
|
64 --
|
|
|
65 -- Set of All function from A to B
|
|
|
66 --
|
|
1174
|
67 Funcs : (A B : HOD) → HOD
|
|
|
68 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B))
|
|
|
69 ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
|
|
|
70 lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (A ⊗ B) x
|
|
|
71 lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
|
|
|
72 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (A ⊗ B) k ) (sym x=ψz) (
|
|
|
73 product→ (subst (λ k → odef A k) (sym &iso) az) (subst (λ k → odef B k)
|
|
|
74 (trans (cong (Func.func F) (sym &iso)) (sym &iso)) (Func.is-func F az) ))
|
|
431
|
75
|
|
|
76 record Injection (A B : Ordinal ) : Set n where
|
|
|
77 field
|
|
|
78 i→ : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
79 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt )
|
|
1095
|
80 iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y
|
|
431
|
81
|
|
1124
|
82 record OrdBijection (A B : Ordinal ) : Set n where
|
|
431
|
83 field
|
|
|
84 fun← : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
85 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal
|
|
|
86 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt )
|
|
|
87 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt )
|
|
|
88 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
|
|
|
89 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
|
|
1095
|
90
|
|
1124
|
91 ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
|
|
|
92 ordbij-refl {a} refl = record {
|
|
|
93 fun← = λ x _ → x
|
|
|
94 ; fun→ = λ x _ → x
|
|
|
95 ; funB = λ x lt → lt
|
|
|
96 ; funA = λ x lt → lt
|
|
|
97 ; fiso← = λ x lt → refl
|
|
|
98 ; fiso→ = λ x lt → refl
|
|
|
99 }
|
|
|
100
|
|
1095
|
101 open Injection
|
|
1124
|
102 open OrdBijection
|
|
1095
|
103
|
|
|
104 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
|
|
|
105 field
|
|
|
106 ax : odef (* a) x
|
|
|
107 bx : odef (* b) (i→ iab _ ax)
|
|
|
108
|
|
|
109 Image : { a b : Ordinal } → Injection a b → HOD
|
|
|
110 Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = a ; <odmax = λ lt → ? }
|
|
|
111
|
|
|
112 image=a : ?
|
|
|
113 image=a = ?
|
|
431
|
114
|
|
|
115 _=c=_ : ( A B : HOD ) → Set n
|
|
1124
|
116 A =c= B = OrdBijection ( & A ) ( & B )
|
|
431
|
117
|
|
1095
|
118 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
|
|
|
119 c=→≡ = ?
|
|
|
120
|
|
|
121 ≡→c= : {A B : HOD} → A ≡ B → A =c= B
|
|
|
122 ≡→c= = ?
|
|
|
123
|
|
1124
|
124 open import BAlgebra O
|
|
|
125
|
|
|
126 _-_ : (a b : Ordinal ) → Ordinal
|
|
|
127 a - b = & ( (* a) ＼ (* b) )
|
|
|
128
|
|
|
129 -→< : (a b : Ordinal ) → (a - b) o≤ a
|
|
|
130 -→< a b = ?
|
|
|
131
|
|
|
132 Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧ Injection b a → Injection (b - a) b ∧ Injection b (b - a)
|
|
|
133 Bernstein1 = ?
|
|
|
134
|
|
|
135 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
|
|
|
136 Bernstein {a} {b} iab iba = be00 where
|
|
1095
|
137 a⊆b : * a ⊆ * b
|
|
1124
|
138 a⊆b {x} ax = subst (λ k → odef (* b) k) be01 ( iB iab _ ax ) where
|
|
|
139 be01 : i→ iab x ax ≡ x
|
|
|
140 be01 = ?
|
|
|
141 be02 : x ≡ i→ iba x ?
|
|
|
142 be02 = iiso iab ? ? ax ( iB iba _ ? ) ?
|
|
1095
|
143 b⊆a : * b ⊆ * a
|
|
|
144 b⊆a bx = ?
|
|
1124
|
145 be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥
|
|
|
146 be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ }
|
|
|
147 ind a b a<b iab iba where
|
|
|
148 ind :(x : Ordinal) →
|
|
|
149 ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
|
|
|
150 (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥
|
|
|
151 ind x prev b x<b ixb ibx = ?
|
|
|
152 be00 : OrdBijection a b
|
|
|
153 be00 with trio< a b
|
|
|
154 ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
|
|
|
155 ... | tri≈ ¬a b ¬c = ordbij-refl b
|
|
|
156 ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )
|
|
1095
|
157
|
|
431
|
158 _c<_ : ( A B : HOD ) → Set n
|
|
|
159 A c< B = ¬ ( Injection (& A) (& B) )
|
|
|
160
|
|
|
161 Card : OD
|
|
1124
|
162 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
|
|
431
|
163
|
|
|
164 record Cardinal (a : Ordinal ) : Set (suc n) where
|
|
|
165 field
|
|
|
166 card : Ordinal
|
|
1124
|
167 ciso : OrdBijection a card
|
|
|
168 cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x
|
|
431
|
169
|
|
1095
|
170 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t
|
|
431
|
171 Cardinal∈ = {!!}
|
|
|
172
|
|
|
173 Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t )
|
|
|
174 Cardinal⊆ = {!!}
|
|
|
175
|
|
|
176 Cantor1 : { u : HOD } → u c< Power u
|
|
|
177 Cantor1 = {!!}
|
|
|
178
|
|
|
179 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
|
|
|
180 Cantor2 = {!!}
|
|
1095
|
181
|
|
|
182
|
|
|
183
|
|
|
184
|
