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

comparison cardinal.agda @ 425:f7d66c84bc26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Aug 2020 19:37:07 +0900
parents cc7909f86841
children 47aacf417930
comparison
equal deleted inserted replaced
424:cc7909f86841 425:f7d66c84bc26
47 FuncP : ( A B : HOD ) → HOD 47 FuncP : ( A B : HOD ) → HOD
48 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x 48 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
49 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } 49 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
50 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) } 50 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
51 51
52 Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) 52 -- Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
53 → def Func (& (Replace A (λ x → < x , f x > ))) 53 -- → def Func (& (Replace A (λ x → < x , f x > )))
54 Func∋f = {!!} 54 -- Func∋f = {!!}
55 55
56 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) 56 -- FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
57 → odef (FuncP A B) (& (Replace A (λ x → < x , f x > ))) 57 -- → odef (FuncP A B) (& (Replace A (λ x → < x , f x > )))
58 FuncP∋f = {!!} 58 -- FuncP∋f = {!!}
59 59
60 -- Func→f : {A B f x : HOD} → def Func (& f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) 60 -- Func→f : {A B f x : HOD} → def Func (& f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))
61 -- Func→f = {!!} 61 -- Func→f = {!!}
62 -- Func₁ : {A B f : HOD} → def Func (& f) → {!!} 62 -- Func₁ : {A B f : HOD} → def Func (& f) → {!!}
63 -- Func₁ = {!!} 63 -- Func₁ = {!!}
66 -- 1-1 : {A B f : HOD} → def Func (& f) → {!!} 66 -- 1-1 : {A B f : HOD} → def Func (& f) → {!!}
67 -- 1-1 = {!!} 67 -- 1-1 = {!!}
68 -- onto : {A B f : HOD} → def Func (& f) → {!!} 68 -- onto : {A B f : HOD} → def Func (& f) → {!!}
69 -- onto = {!!} 69 -- onto = {!!}
70 70
71 record Injection (A B : Ordinal ) : Set n where
72 field
73 i→ : (x : Ordinal ) → odef (* B) x → Ordinal
74 iA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( i→ x lt )
75 iiso : (x y : Ordinal ) → ( ltx : odef (* B) x ) ( lty : odef (* B) y ) → i→ x ltx ≡ i→ y lty → x ≡ y
76
71 record Bijection (A B : Ordinal ) : Set n where 77 record Bijection (A B : Ordinal ) : Set n where
72 field 78 field
73 fun→ : Ordinal → Ordinal 79 fun← : (x : Ordinal ) → odef (* A) x → Ordinal
74 fun← : Ordinal → Ordinal 80 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal
75 fun→inA : (x : Ordinal) → odef (* A) ( fun→ x ) 81 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt )
76 fun←inB : (x : Ordinal) → odef (* B) ( fun← x ) 82 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt )
77 fiso→ : (x : Ordinal ) → odef (* B) x → fun→ ( fun← x ) ≡ x 83 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
78 fiso← : (x : Ordinal ) → odef (* A) x → fun← ( fun→ x ) ≡ x 84 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
79 85
86 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b
87 Bernstein = {!!}
88
89 _=c=_ : ( A B : HOD ) → Set n
90 A =c= B = Bijection ( & A ) ( & B )
91
92 _c<_ : ( A B : HOD ) → Set n
93 A c< B = Injection (& A) (& B)
94
80 Card : OD 95 Card : OD
81 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } 96 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
97
98 record Cardinal (a : Ordinal ) : Set (suc n) where
99 field
100 card : Ordinal
101 ciso : Bijection a card
102 cmax : (x : Ordinal) → card o< x → ¬ Bijection a x
103
104 Cantor1 : { u : HOD } → u c< Power u
105 Cantor1 = {!!}
106
107 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
108 Cantor2 = {!!}