Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate cardinal.agda @ 425:f7d66c84bc26
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Aug 2020 19:37:07 +0900 |
| parents | cc7909f86841 |
| children | 47aacf417930 |
| rev | line source |
|---|---|
| 16 | 1 open import Level |
| 224 | 2 open import Ordinals |
| 3 module cardinal {n : Level } (O : Ordinals {n}) where | |
| 3 | 4 |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
5 open import zf |
| 219 | 6 open import logic |
| 224 | 7 import OD |
| 276 | 8 import ODC |
| 274 | 9 import OPair |
| 23 | 10 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 224 | 11 open import Relation.Binary.PropositionalEquality |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
12 open import Data.Nat.Properties |
| 6 | 13 open import Data.Empty |
| 14 open import Relation.Nullary | |
| 15 open import Relation.Binary | |
| 16 open import Relation.Binary.Core | |
| 17 | |
| 224 | 18 open inOrdinal O |
| 19 open OD O | |
| 219 | 20 open OD.OD |
| 274 | 21 open OPair O |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
22 open ODAxiom odAxiom |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
23 |
| 424 | 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 | |
| 120 | 33 open _∧_ |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
34 open _∨_ |
|
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
35 open Bool |
| 254 | 36 open _==_ |
|
44
fcac01485f32
od→lv : {n : Level} → OD {n} → Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
37 |
| 420 | 38 open HOD |
| 39 | |
| 416 | 40 -- _⊗_ : (A B : HOD) → HOD |
| 41 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) | |
| 233 | 42 |
| 420 | 43 Func : OD |
| 44 Func = record { def = λ x → def ZFProduct x | |
| 422 | 45 ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } |
| 225 | 46 |
| 420 | 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 | |
| 425 | 52 -- Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) |
| 53 -- → def Func (& (Replace A (λ x → < x , f x > ))) | |
| 54 -- Func∋f = {!!} | |
| 233 | 55 |
| 425 | 56 -- FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) |
| 57 -- → odef (FuncP A B) (& (Replace A (λ x → < x , f x > ))) | |
| 58 -- FuncP∋f = {!!} | |
| 420 | 59 |
| 422 | 60 -- Func→f : {A B f x : HOD} → def Func (& f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) |
| 421 | 61 -- Func→f = {!!} |
| 422 | 62 -- Func₁ : {A B f : HOD} → def Func (& f) → {!!} |
| 421 | 63 -- Func₁ = {!!} |
| 422 | 64 -- Cod : {A B f : HOD} → def Func (& f) → {!!} |
| 421 | 65 -- Cod = {!!} |
| 422 | 66 -- 1-1 : {A B f : HOD} → def Func (& f) → {!!} |
| 421 | 67 -- 1-1 = {!!} |
| 422 | 68 -- onto : {A B f : HOD} → def Func (& f) → {!!} |
| 421 | 69 -- onto = {!!} |
| 227 | 70 |
| 425 | 71 record Injection (A B : Ordinal ) : Set n where |
| 72 field | |
| 73 i→ : (x : Ordinal ) → odef (* B) x → Ordinal | |
| 74 iA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( i→ x lt ) | |
| 75 iiso : (x y : Ordinal ) → ( ltx : odef (* B) x ) ( lty : odef (* B) y ) → i→ x ltx ≡ i→ y lty → x ≡ y | |
| 76 | |
| 416 | 77 record Bijection (A B : Ordinal ) : Set n where |
| 219 | 78 field |
| 425 | 79 fun← : (x : Ordinal ) → odef (* A) x → Ordinal |
| 80 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal | |
| 81 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt ) | |
| 82 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt ) | |
| 83 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x | |
| 84 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x | |
| 416 | 85 |
| 425 | 86 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b |
| 87 Bernstein = {!!} | |
| 88 | |
| 89 _=c=_ : ( A B : HOD ) → Set n | |
| 90 A =c= B = Bijection ( & A ) ( & B ) | |
| 91 | |
| 92 _c<_ : ( A B : HOD ) → Set n | |
| 93 A c< B = Injection (& A) (& B) | |
| 94 | |
| 416 | 95 Card : OD |
| 96 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } | |
| 425 | 97 |
| 98 record Cardinal (a : Ordinal ) : Set (suc n) where | |
| 99 field | |
| 100 card : Ordinal | |
| 101 ciso : Bijection a card | |
| 102 cmax : (x : Ordinal) → card o< x → ¬ Bijection a x | |
| 103 | |
| 104 Cantor1 : { u : HOD } → u c< Power u | |
| 105 Cantor1 = {!!} | |
| 106 | |
| 107 Cantor2 : { u : HOD } → ¬ ( u =c= Power u ) | |
| 108 Cantor2 = {!!} |