Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate cardinal.agda @ 417:f464e48e18cc
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 Jul 2020 11:21:27 +0900 |
| parents | b737a2e0b46e |
| children | 53422a8ea836 |
| 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 |
| 120 | 24 open _∧_ |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
25 open _∨_ |
|
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
26 open Bool |
| 254 | 27 open _==_ |
|
44
fcac01485f32
od→lv : {n : Level} → OD {n} → Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
28 |
| 416 | 29 -- _⊗_ : (A B : HOD) → HOD |
| 30 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) | |
| 233 | 31 |
| 416 | 32 Func : ( A B : HOD ) → OD |
| 33 Func A B = record { def = λ x → (odef (Power (A ⊗ B)) x) | |
| 34 ∧ ( (a b c : Ordinal) → odef (ord→od x) (od→ord < ord→od a , ord→od b >) ∧ odef (ord→od x) (od→ord < ord→od a , ord→od c >) → b ≡ c ) } | |
| 225 | 35 |
| 416 | 36 Func∋f : {A B x : HOD} → ( f : (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))) → (lt : A ∋ x ) → def (Func A B ) (od→ord < x , proj1 (f x lt) > ) |
| 37 Func∋f = {!!} | |
| 233 | 38 |
| 416 | 39 Func→f : {A B f x : HOD} → def ( Func A B) (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) |
| 40 Func→f = {!!} | |
| 233 | 41 |
| 416 | 42 Func₁ : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} |
| 43 Func₁ = {!!} | |
| 240 | 44 |
| 416 | 45 Cod : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} |
| 46 Cod = {!!} | |
| 240 | 47 |
| 416 | 48 1-1 : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} |
| 49 1-1 = {!!} | |
| 227 | 50 |
| 416 | 51 onto : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} |
| 52 onto = {!!} | |
| 227 | 53 |
| 416 | 54 record Bijection (A B : Ordinal ) : Set n where |
| 219 | 55 field |
| 416 | 56 bfun : Ordinal |
| 417 | 57 bfun-isfun : def (Func (ord→od A) (ord→od B)) bfun |
| 58 bfun-is1-1 : {!!} | |
| 59 bfun-isonto : {!!} | |
| 416 | 60 |
| 61 Card : OD | |
| 62 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } |