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

comparison cardinal.agda @ 420:53422a8ea836

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bijection
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Jul 2020 17:42:25 +0900
parents f464e48e18cc
children cb067605fea0
comparison
equal deleted inserted replaced
419:4af94768e372 420:53422a8ea836
24 open _∧_ 24 open _∧_
25 open _∨_ 25 open _∨_
26 open Bool 26 open Bool
27 open _==_ 27 open _==_
28 28
29 open HOD
30
29 -- _⊗_ : (A B : HOD) → HOD 31 -- _⊗_ : (A B : HOD) → HOD
30 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) 32 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
31 33
32 Func : ( A B : HOD ) → OD 34 Func : OD
33 Func A B = record { def = λ x → (odef (Power (A ⊗ B)) x) 35 Func = record { def = λ x → def ZFProduct x
34 ∧ ( (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 ) } 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 ) }
35 37
36 Func∋f : {A B x : HOD} → ( f : (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))) → (lt : A ∋ x ) → def (Func A B ) (od→ord < x , proj1 (f x lt) > ) 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 > )))
37 Func∋f = {!!} 45 Func∋f = {!!}
38 46
39 Func→f : {A B f x : HOD} → def ( Func A B) (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) 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 ))
40 Func→f = {!!} 52 Func→f = {!!}
41 53
42 Func₁ : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} 54 Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}
43 Func₁ = {!!} 55 Func₁ = {!!}
44 56
45 Cod : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} 57 Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
46 Cod = {!!} 58 Cod = {!!}
47 59
48 1-1 : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} 60 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
49 1-1 = {!!} 61 1-1 = {!!}
50 62
51 onto : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} 63 onto : {A B f : HOD} → def Func (od→ord f) → {!!}
52 onto = {!!} 64 onto = {!!}
53 65
54 record Bijection (A B : Ordinal ) : Set n where 66 record Bijection (A B : Ordinal ) : Set n where
55 field 67 field
56 bfun : Ordinal 68 fun→ : Ordinal → Ordinal
57 bfun-isfun : def (Func (ord→od A) (ord→od B)) bfun 69 fun← : Ordinal → Ordinal
58 bfun-is1-1 : {!!} 70 fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
59 bfun-isonto : {!!} 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
60 74
61 Card : OD 75 Card : OD
62 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } 76 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }