|
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
|
|
|
7 import OD
|
|
|
8 import ODC
|
|
|
9 import OPair
|
|
|
10 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
11 open import Relation.Binary.PropositionalEquality
|
|
|
12 open import Data.Nat.Properties
|
|
|
13 open import Data.Empty
|
|
|
14 open import Relation.Nullary
|
|
|
15 open import Relation.Binary
|
|
|
16 open import Relation.Binary.Core
|
|
|
17
|
|
|
18 open inOrdinal O
|
|
|
19 open OD O
|
|
|
20 open OD.OD
|
|
|
21 open OPair O
|
|
|
22 open ODAxiom odAxiom
|
|
|
23
|
|
|
24 import OrdUtil
|
|
|
25 import ODUtil
|
|
|
26 open Ordinals.Ordinals O
|
|
|
27 open Ordinals.IsOrdinals isOrdinal
|
|
|
28 open Ordinals.IsNext isNext
|
|
|
29 open OrdUtil O
|
|
|
30 open ODUtil O
|
|
|
31
|
|
|
32
|
|
|
33 open _∧_
|
|
|
34 open _∨_
|
|
|
35 open Bool
|
|
|
36 open _==_
|
|
|
37
|
|
|
38 open HOD
|
|
|
39
|
|
|
40 -- _⊗_ : (A B : HOD) → HOD
|
|
|
41 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
|
|
|
42
|
|
|
43 Func : OD
|
|
|
44 Func = record { def = λ x → def ZFProduct x
|
|
|
45 ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) }
|
|
|
46
|
|
|
47 FuncP : ( A B : HOD ) → HOD
|
|
|
48 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
|
|
|
49 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
|
|
|
50 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
|
|
|
51
|
|
|
52 record Injection (A B : Ordinal ) : Set n where
|
|
|
53 field
|
|
|
54 i→ : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
55 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt )
|
|
|
56 iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y
|
|
|
57
|
|
|
58 record Bijection (A B : Ordinal ) : Set n where
|
|
|
59 field
|
|
|
60 fun← : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
61 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal
|
|
|
62 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt )
|
|
|
63 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt )
|
|
|
64 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
|
|
|
65 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
|
|
|
66
|
|
|
67 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b
|
|
|
68 Bernstein = {!!}
|
|
|
69
|
|
|
70 _=c=_ : ( A B : HOD ) → Set n
|
|
|
71 A =c= B = Bijection ( & A ) ( & B )
|
|
|
72
|
|
|
73 _c<_ : ( A B : HOD ) → Set n
|
|
|
74 A c< B = ¬ ( Injection (& A) (& B) )
|
|
|
75
|
|
|
76 Card : OD
|
|
|
77 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
|
|
|
78
|
|
|
79 record Cardinal (a : Ordinal ) : Set (suc n) where
|
|
|
80 field
|
|
|
81 card : Ordinal
|
|
|
82 ciso : Bijection a card
|
|
|
83 cmax : (x : Ordinal) → card o< x → ¬ Bijection a x
|
|
|
84
|
|
|
85 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t
|
|
|
86 Cardinal∈ = {!!}
|
|
|
87
|
|
|
88 Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t )
|
|
|
89 Cardinal⊆ = {!!}
|
|
|
90
|
|
|
91 Cantor1 : { u : HOD } → u c< Power u
|
|
|
92 Cantor1 = {!!}
|
|
|
93
|
|
|
94 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
|
|
|
95 Cantor2 = {!!}
|
