Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison cardinal.agda @ 219:43021d2b8756

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate cardinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Aug 2019 09:50:51 +0900
parents OD.agda@eee983e4b402
children afc864169325
comparison
equal deleted inserted replaced
218:eee983e4b402 219:43021d2b8756
1 open import Level
2 module cardinal where
3
4 open import zf
5 open import ordinal
6 open import logic
7 open import OD
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9 open import Relation.Binary.PropositionalEquality
10 open import Data.Nat.Properties
11 open import Data.Empty
12 open import Relation.Nullary
13 open import Relation.Binary
14 open import Relation.Binary.Core
15
16 open OD.OD
17
18 open Ordinal
19 open _∧_
20 open _∨_
21 open Bool
22
23 ------------
24 --
25 -- Onto map
26 -- def X x -> xmap
27 -- X ---------------------------> Y
28 -- ymap <- def Y y
29 --
30 record Onto {n : Level } (X Y : OD {n}) : Set (suc n) where
31 field
32 xmap : (x : Ordinal {n}) → def X x → Ordinal {n}
33 ymap : (y : Ordinal {n}) → def Y y → Ordinal {n}
34 ymap-on-X : {y : Ordinal {n} } → (lty : def Y y ) → def X (ymap y lty)
35 onto-iso : {y : Ordinal {n} } → (lty : def Y y ) → xmap ( ymap y lty ) (ymap-on-X lty ) ≡ y
36
37 record Cardinal {n : Level } (X : OD {n}) : Set (suc n) where
38 field
39 cardinal : Ordinal {n}
40 conto : Onto (Ord cardinal) X
41 cmax : ( y : Ordinal {n} ) → cardinal o< y → ¬ Onto (Ord y) X
42
43 cardinal : {n : Level } (X : OD {suc n}) → Cardinal X
44 cardinal {n} X = record {
45 cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
46 ; conto = onto
47 ; cmax = cmax
48 } where
49 cardinal-p : (x : Ordinal {suc n}) → ( Ordinal {suc n} ∧ Dec (Onto (Ord x) X) )
50 cardinal-p x with p∨¬p ( Onto (Ord x) X )
51 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
52 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
53 onto-set : OD {suc n}
54 onto-set = record { def = λ x → {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X }
55 onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
56 onto = record {
57 xmap = xmap
58 ; ymap = ymap
59 ; ymap-on-X = ymap-on-X
60 ; onto-iso = onto-iso
61 } where
62 --
63 -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one
64 -- od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X
65 Y = (Ord (sup-o (λ x → proj1 (cardinal-p x))))
66 lemma1 : (y : Ordinal {suc n}) → def Y y → Onto (Ord y) X
67 lemma1 y y<Y with sup-o< {suc n} {λ x → proj1 ( cardinal-p x)} {y}
68 ... | t = {!!}
69 lemma2 : def Y (od→ord X)
70 lemma2 = {!!}
71 xmap : (x : Ordinal {suc n}) → def Y x → Ordinal {suc n}
72 xmap = {!!}
73 ymap : (y : Ordinal {suc n}) → def X y → Ordinal {suc n}
74 ymap = {!!}
75 ymap-on-X : {y : Ordinal {suc n} } → (lty : def X y ) → def Y (ymap y lty)
76 ymap-on-X = {!!}
77 onto-iso : {y : Ordinal {suc n} } → (lty : def X y ) → xmap (ymap y lty) (ymap-on-X lty ) ≡ y
78 onto-iso = {!!}
79 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
80 cmax y lt ontoy = o<> lt (o<-subst {suc n} {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
81 (sup-o< {suc n} {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where
82 lemma : proj1 (cardinal-p y) ≡ y
83 lemma with p∨¬p ( Onto (Ord y) X )
84 lemma | case1 x = refl
85 lemma | case2 not = ⊥-elim ( not ontoy )
86
87 func : {n : Level} → (f : Ordinal {suc n} → Ordinal {suc n}) → OD {suc n}
88 func {n} f = record { def = λ y → (x : Ordinal {suc n}) → y ≡ f x }
89
90 Func : {n : Level} → OD {suc n}
91 Func {n} = record { def = λ x → (f : Ordinal {suc n} → Ordinal {suc n}) → x ≡ od→ord (func f) }
92
93 odmap : {n : Level} → { x : OD {suc n} } → Func ∋ x → Ordinal {suc n} → OD {suc n}
94 odmap {n} {f} lt x = record { def = λ y → def f y }
95
96 lemma1 : {n : Level} → { x : OD {suc n} } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal {suc n} → Ordinal {suc n}) → ¬ ( x ≡ od→ord (func f) ))
97 lemma1 = {!!}
98
99
100 -----
101 -- All cardinal is ℵ0, since we are working on Countable Ordinal,
102 -- Power ω is larger than ℵ0, so it has no cardinal.
103
104
105