annotate cardinal.agda @ 236:650bdad56729

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Aug 2019 15:53:29 +0900
parents 846e0926bb89
children 521290e85527
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
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
8 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
9 open import Relation.Binary.PropositionalEquality
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
10 open import Data.Nat.Properties
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
14 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
15
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
16 open inOrdinal O
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
17 open OD O
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
18 open OD.OD
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
19
120
ac214eab1c3c inifinite done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 119
diff changeset
20 open _∧_
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
21 open _∨_
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
22 open Bool
44
fcac01485f32 od→lv : {n : Level} → OD {n} → Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 43
diff changeset
23
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
24 -- we have to work on Ordinal to keep OD Level n
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
25 -- since we use p∨¬p which works only on Level n
225
5f48299929ac does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
26
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
27 <_,_> : (x y : OD) → OD
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
28 < x , y > = (x , x ) , (x , y )
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
29
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
30 record SetProduct ( A B : OD ) : Set n where
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
31 field
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
32 π1 : Ordinal
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
33 π2 : Ordinal
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
34 A∋π1 : def A π1
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
35 B∋π2 : def B π2
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
36 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 >
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
37
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
38 open SetProduct
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
39
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
40 ∋-p : (A x : OD ) → Dec ( A ∋ x )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
41 ∋-p A x with p∨¬p ( A ∋ x )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
42 ∋-p A x | case1 t = yes t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
43 ∋-p A x | case2 t = no t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
44
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
45 _⊗_ : (A B : OD) → OD
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
46 A ⊗ B = record { def = λ x → SetProduct A B }
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
47 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
48
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
49 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
225
5f48299929ac does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
50
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
51 Func : ( A B : OD ) → OD
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
52 Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
53
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
54 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
55
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
56 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal )
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
57 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
58 lemma : Ordinal → Ordinal
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
59 lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
60 lemma y | p | no n = o∅
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
61 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
62 ... | t with decp ( x ≡ π1 t )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
63 ... | yes _ = π2 t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
64 ... | no _ = o∅
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
65
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
66
233
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
67 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
68 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
af60c40298a4 function continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 230
diff changeset
69
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
70 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
71 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
72 func-1 : Ordinal → Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
73 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
75 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
76 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
77 lemma : Ordinal → Ordinal → Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
78 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
79 lemma x y | p | no n = o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
80 lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
81 ... | t with decp ( x ≡ π1 t )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
82 ... | yes _ = π2 t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
83 ... | no _ = o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
84
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
85 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
86 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} }
225
5f48299929ac does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
87
227
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
88 -- contra position of sup-o<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
89 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
90
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
91 -- postulate
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
92 -- -- contra-position of mimimulity of supermum required in Cardinal
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
93 -- sup-x : ( Ordinal → Ordinal ) → Ordinal
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
94 -- sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
227
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 226
diff changeset
95
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
96 ------------
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
97 --
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
98 -- Onto map
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
99 -- def X x -> xmap
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
100 -- X ---------------------------> Y
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
101 -- ymap <- def Y y
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
102 --
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
103 record Onto (X Y : OD ) : Set n where
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
104 field
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
105 xmap : Ordinal
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
106 ymap : Ordinal
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
107 xfunc : def (Func X Y) xmap
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
108 yfunc : def (Func Y X) ymap
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
109 onto-iso : {y : Ordinal } → (lty : def Y y ) →
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
110 func←od {X} {Y} {xmap} xfunc ( func←od yfunc y ) ≡ y
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
111
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
112 open Onto
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
113
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
114 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
115 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
116 xmap = xmap1
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
117 ; ymap = zmap
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
118 ; xfunc = xfunc1
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
119 ; yfunc = zfunc
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
120 ; onto-iso = onto-iso1
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
121 } where
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
122 xmap1 : Ordinal
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
123 xmap1 = od→ord (Select (ord→od (xmap onto)) {!!} )
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
124 zmap : Ordinal
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
125 zmap = {!!}
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
126 xfunc1 : def (Func X Z) xmap1
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
127 xfunc1 = {!!}
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
128 zfunc : def (Func Z X) zmap
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
129 zfunc = {!!}
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
130 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od xfunc1 ( func←od zfunc z ) ≡ z
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
131 onto-iso1 = {!!}
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
132
51
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
133
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
134 record Cardinal (X : OD ) : Set n where
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
135 field
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
136 cardinal : Ordinal
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
137 conto : Onto X (Ord cardinal)
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
138 cmax : ( y : Ordinal ) → cardinal o< y → ¬ Onto X (Ord y)
151
b5a337fb7a6d recovering...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 150
diff changeset
139
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
140 cardinal : (X : OD ) → Cardinal X
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
141 cardinal X = record {
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
142 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
143 ; conto = onto
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
144 ; cmax = cmax
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
145 } where
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
146 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto X (Ord x) ) )
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
147 cardinal-p x with p∨¬p ( Onto X (Ord x) )
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
148 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
149 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
229
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
150 S = sup-o (λ x → proj1 (cardinal-p x))
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
151 lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
152 Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
229
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
153 lemma1 x prev with trio< x (osuc S)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
154 lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
155 lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} )
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
156 lemma1 x prev | tri< a ¬b ¬c | case2 x<S = lift ( λ lt → lemma2 ) where
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
157 lemma2 : Onto X (Ord x)
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
158 lemma2 with prev {!!} {!!}
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
159 ... | lift t = t {!!}
229
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
160 lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
161 lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
162 onto : Onto X (Ord S)
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
163 onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
164 ... | lift t = t <-osuc
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
165 cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y)
229
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
166 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S}
224
afc864169325 recover ε-induction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
167 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
168 lemma : proj1 (cardinal-p y) ≡ y
230
1b1620e2053c we need ordered pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
169 lemma with p∨¬p ( Onto X (Ord y) )
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
170 lemma | case1 x = refl
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
171 lemma | case2 not = ⊥-elim ( not ontoy )
217
d5668179ee69 cardinal continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 216
diff changeset
172
226
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
173
176ff97547b4 set theortic function definition using sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
174 -----
219
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
175 -- All cardinal is ℵ0, since we are working on Countable Ordinal,
43021d2b8756 separate cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
176 -- Power ω is larger than ℵ0, so it has no cardinal.
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 217
diff changeset
177
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 217
diff changeset
178
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 217
diff changeset
179