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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
1 open import Level
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
2 open import Ordinals
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
3 module cardinal {n : Level } (O : Ordinals {n}) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
5 open import zf
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
6 open import logic
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
7 import OD
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
8 import ODC
274
29a85a427ed2 ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
9 import OPair
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
10 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
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
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
14 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
15 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
16 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
17
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
18 open inOrdinal O
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
19 open OD O
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
20 open OD.OD
274
29a85a427ed2 ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
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
ac214eab1c3c inifinite done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
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
2ea2a19f9cd6 ordered pair clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
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
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
29 open HOD
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
30
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
31 -- _⊗_ : (A B : HOD) → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
32 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
33
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
34 Func : OD
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
35 Func = record { def = λ x → def ZFProduct x
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
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
5f48299929ac does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
37
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
38 FuncP : ( A B : HOD ) → HOD
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
39 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
40 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
41 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
42
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
43 Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
44 → def Func (od→ord (Replace A (λ x → < x , f x > )))
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
45 Func∋f = {!!}
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
46
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
47 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
48 → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > )))
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
49 FuncP∋f = {!!}
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
50
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
51 Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
52 Func→f = {!!}
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
53
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
54 Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
55 Func₁ = {!!}
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
56
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
57 Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
58 Cod = {!!}
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
59
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
60 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
61 1-1 = {!!}
227
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
62
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
63 onto : {A B f : HOD} → def Func (od→ord f) → {!!}
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
64 onto = {!!}
227
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
65
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
66 record Bijection (A B : Ordinal ) : Set n where
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
67 field
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
68 fun→ : Ordinal → Ordinal
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
69 fun← : Ordinal → Ordinal
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
70 fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
71 fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x )
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
72 fiso→ : (x : Ordinal ) → odef (ord→od A) x → fun→ ( fun← x ) ≡ x
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
73 fiso← : (x : Ordinal ) → odef (ord→od B) x → fun← ( fun→ x ) ≡ x
416
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
75 Card : OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 378
diff changeset
76 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }