Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate cardinal.agda @ 420:53422a8ea836
bijection
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 31 Jul 2020 17:42:25 +0900 |
parents | f464e48e18cc |
children | cb067605fea0 |
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 |
420 | 29 open HOD |
30 | |
416 | 31 -- _⊗_ : (A B : HOD) → HOD |
32 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) | |
233 | 33 |
420 | 34 Func : OD |
35 Func = record { def = λ x → def ZFProduct x | |
416 | 36 ∧ ( (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 | 37 |
420 | 38 FuncP : ( A B : HOD ) → HOD |
39 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x | |
40 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } | |
41 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) } | |
42 | |
43 Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) | |
44 → def Func (od→ord (Replace A (λ x → < x , f x > ))) | |
416 | 45 Func∋f = {!!} |
233 | 46 |
420 | 47 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) |
48 → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > ))) | |
49 FuncP∋f = {!!} | |
50 | |
51 Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) | |
416 | 52 Func→f = {!!} |
233 | 53 |
420 | 54 Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!} |
416 | 55 Func₁ = {!!} |
240 | 56 |
420 | 57 Cod : {A B f : HOD} → def Func (od→ord f) → {!!} |
416 | 58 Cod = {!!} |
240 | 59 |
420 | 60 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!} |
416 | 61 1-1 = {!!} |
227 | 62 |
420 | 63 onto : {A B f : HOD} → def Func (od→ord f) → {!!} |
416 | 64 onto = {!!} |
227 | 65 |
416 | 66 record Bijection (A B : Ordinal ) : Set n where |
219 | 67 field |
420 | 68 fun→ : Ordinal → Ordinal |
69 fun← : Ordinal → Ordinal | |
70 fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x ) | |
71 fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x ) | |
72 fiso→ : (x : Ordinal ) → odef (ord→od A) x → fun→ ( fun← x ) ≡ x | |
73 fiso← : (x : Ordinal ) → odef (ord→od B) x → fun← ( fun→ x ) ≡ x | |
416 | 74 |
75 Card : OD | |
76 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } |