|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 module cardinal {n : Level } (O : Ordinals {n}) where
|
|
|
4
|
|
|
5 open import zf
|
|
|
6 open import logic
|
|
1095
|
7 -- import OD
|
|
|
8 import OD hiding ( _⊆_ )
|
|
|
9
|
|
431
|
10 import ODC
|
|
|
11 import OPair
|
|
1095
|
12 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
431
|
13 open import Relation.Binary.PropositionalEquality
|
|
1095
|
14 open import Data.Nat.Properties
|
|
431
|
15 open import Data.Empty
|
|
|
16 open import Relation.Nullary
|
|
|
17 open import Relation.Binary
|
|
|
18 open import Relation.Binary.Core
|
|
|
19
|
|
|
20 open inOrdinal O
|
|
|
21 open OD O
|
|
|
22 open OD.OD
|
|
|
23 open OPair O
|
|
|
24 open ODAxiom odAxiom
|
|
|
25
|
|
|
26 import OrdUtil
|
|
|
27 import ODUtil
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
|
30 open Ordinals.IsNext isNext
|
|
|
31 open OrdUtil O
|
|
|
32 open ODUtil O
|
|
|
33
|
|
1095
|
34 _⊆_ : ( A B : HOD ) → Set n
|
|
|
35 _⊆_ A B = {x : Ordinal } → odef A x → odef B x
|
|
|
36
|
|
431
|
37
|
|
|
38 open _∧_
|
|
|
39 open _∨_
|
|
|
40 open Bool
|
|
|
41 open _==_
|
|
|
42
|
|
|
43 open HOD
|
|
|
44
|
|
|
45 -- _⊗_ : (A B : HOD) → HOD
|
|
|
46 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
|
|
|
47
|
|
|
48 Func : OD
|
|
|
49 Func = record { def = λ x → def ZFProduct x
|
|
1095
|
50 ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) }
|
|
431
|
51
|
|
|
52 FuncP : ( A B : HOD ) → HOD
|
|
|
53 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
|
|
1095
|
54 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
|
|
431
|
55 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
|
|
|
56
|
|
|
57 record Injection (A B : Ordinal ) : Set n where
|
|
|
58 field
|
|
|
59 i→ : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
60 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt )
|
|
1095
|
61 iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y
|
|
431
|
62
|
|
|
63 record Bijection (A B : Ordinal ) : Set n where
|
|
|
64 field
|
|
|
65 fun← : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
66 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal
|
|
|
67 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt )
|
|
|
68 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt )
|
|
|
69 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
|
|
|
70 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
|
|
1095
|
71
|
|
|
72 open Injection
|
|
|
73 open Bijection
|
|
|
74
|
|
|
75 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
|
|
|
76 field
|
|
|
77 ax : odef (* a) x
|
|
|
78 bx : odef (* b) (i→ iab _ ax)
|
|
|
79
|
|
|
80 Image : { a b : Ordinal } → Injection a b → HOD
|
|
|
81 Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = a ; <odmax = λ lt → ? }
|
|
|
82
|
|
|
83 image=a : ?
|
|
|
84 image=a = ?
|
|
431
|
85
|
|
|
86 _=c=_ : ( A B : HOD ) → Set n
|
|
|
87 A =c= B = Bijection ( & A ) ( & B )
|
|
|
88
|
|
1095
|
89 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
|
|
|
90 c=→≡ = ?
|
|
|
91
|
|
|
92 ≡→c= : {A B : HOD} → A ≡ B → A =c= B
|
|
|
93 ≡→c= = ?
|
|
|
94
|
|
|
95 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b
|
|
|
96 Bernstein {a} {b} iab iba = {!!} where
|
|
|
97 a⊆b : * a ⊆ * b
|
|
|
98 a⊆b ax = subst (λ k → odef (* b) k) ? ( iB iab _ ax )
|
|
|
99 b⊆a : * b ⊆ * a
|
|
|
100 b⊆a bx = ?
|
|
|
101
|
|
431
|
102 _c<_ : ( A B : HOD ) → Set n
|
|
|
103 A c< B = ¬ ( Injection (& A) (& B) )
|
|
|
104
|
|
|
105 Card : OD
|
|
|
106 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
|
|
|
107
|
|
|
108 record Cardinal (a : Ordinal ) : Set (suc n) where
|
|
|
109 field
|
|
|
110 card : Ordinal
|
|
|
111 ciso : Bijection a card
|
|
|
112 cmax : (x : Ordinal) → card o< x → ¬ Bijection a x
|
|
|
113
|
|
1095
|
114 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t
|
|
431
|
115 Cardinal∈ = {!!}
|
|
|
116
|
|
|
117 Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t )
|
|
|
118 Cardinal⊆ = {!!}
|
|
|
119
|
|
|
120 Cantor1 : { u : HOD } → u c< Power u
|
|
|
121 Cantor1 = {!!}
|
|
|
122
|
|
|
123 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
|
|
|
124 Cantor2 = {!!}
|
|
1095
|
125
|
|
|
126
|
|
|
127
|
|
|
128
|
