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

comparison cardinal.agda @ 239:b6d80eec5f9e

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 Tue, 20 Aug 2019 10:36:37 +0900
parents a8c6239176db
children c76c812de395
comparison
equal deleted inserted replaced
238:a8c6239176db 239:b6d80eec5f9e
31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) 31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
32 32
33 ZFProduct : OD 33 ZFProduct : OD
34 ZFProduct = record { def = λ x → ord-pair x } 34 ZFProduct = record { def = λ x → ord-pair x }
35 35
36 π1' : { p : OD } → ZFProduct ∋ p → OD 36 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
37 π1' lt = ord→od (pi1 lt) where 37 π1 lt = pi1 lt where
38 pi1 : { p : Ordinal } → ord-pair p → Ordinal 38 pi1 : { p : Ordinal } → ord-pair p → Ordinal
39 pi1 ( pair x y ) = x 39 pi1 ( pair x y ) = x
40 40
41 π2' : { p : OD } → ZFProduct ∋ p → OD 41 π2 : { p : OD } → ZFProduct ∋ p → Ordinal
42 π2' lt = ord→od (pi2 lt) where 42 π2 lt = pi2 lt where
43 pi2 : { p : Ordinal } → ord-pair p → Ordinal 43 pi2 : { p : Ordinal } → ord-pair p → Ordinal
44 pi2 ( pair x y ) = y 44 pi2 ( pair x y ) = y
45 45
46 p-cons : { x y : OD } → ZFProduct ∋ < x , y > 46 p-cons : { x y : OD } → ZFProduct ∋ < x , y >
47 p-cons {x} {y} = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( 47 p-cons {x} {y} = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ 50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
51 od→ord < x , y > 51 od→ord < x , y >
52 ∎ ) 52 ∎ )
53 53
54 54
55
56 record SetProduct ( A B : OD ) : Set n where
57 field
58 π1 : Ordinal
59 π2 : Ordinal
60 A∋π1 : def A π1
61 B∋π2 : def B π2
62 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 >
63
64 open SetProduct
65
66 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 55 ∋-p : (A x : OD ) → Dec ( A ∋ x )
67 ∋-p A x with p∨¬p ( A ∋ x ) 56 ∋-p A x with p∨¬p ( A ∋ x )
68 ∋-p A x | case1 t = yes t 57 ∋-p A x | case1 t = yes t
69 ∋-p A x | case2 t = no t 58 ∋-p A x | case2 t = no t
70 59
71 _⊗_ : (A B : OD) → OD 60 _⊗_ : (A B : OD) → OD
72 A ⊗ B = record { def = λ x → SetProduct A B } 61 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
73 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) } 62 checkAB : { p : Ordinal } → def ZFProduct p → Set n
63 checkAB (pair x y) = def A x ∧ def B y
74 64
75 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) 65 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
76 66
77 Func : ( A B : OD ) → OD 67 Func : ( A B : OD ) → OD
78 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } 68 Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
79 69
80 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) 70 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
81
82 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal )
83 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where
84 lemma : Ordinal → Ordinal
85 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)
86 lemma y | p | no n = o∅
87 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
88 ... | t with decp ( x ≡ π1 t )
89 ... | yes _ = π2 t
90 ... | no _ = o∅
91 71
92 72
93 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 73 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
94 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) 74 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
95 75
96 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where 76 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where
97 field 77 field
98 func-1 : Ordinal → Ordinal 78 func-1 : Ordinal → Ordinal
99 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom 79 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom
100 80
81 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal )
82 od→func {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where
83 lemma2 : {p : Ordinal} → ord-pair p → Ordinal
84 lemma2 (pair x1 y1) with decp ( x1 ≡ x)
85 lemma2 (pair x1 y1) | yes p = y1
86 lemma2 (pair x1 y1) | no ¬p = o∅
87 lemma : Ordinal → Ordinal
88 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)
89 lemma y | p | no n = o∅
90 lemma y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
91
101 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F 92 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
102 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where 93 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
103 lemma : Ordinal → Ordinal → Ordinal 94 lemma : Ordinal → Ordinal → Ordinal
104 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) 95 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)
105 lemma x y | p | no n = o∅ 96 lemma x y | p | no n = o∅
106 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) 97 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)
107 ... | t with decp ( x ≡ π1 t ) 98 ... | t with decp ( x ≡ π1 {!!} )
108 ... | yes _ = π2 t 99 ... | yes _ = π2 {!!}
109 ... | no _ = o∅ 100 ... | no _ = o∅
110 101
111 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom 102 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom
112 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } 103 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} }
113 104
131 xmap : Ordinal 122 xmap : Ordinal
132 ymap : Ordinal 123 ymap : Ordinal
133 xfunc : def (Func X Y) xmap 124 xfunc : def (Func X Y) xmap
134 yfunc : def (Func Y X) ymap 125 yfunc : def (Func Y X) ymap
135 onto-iso : {y : Ordinal } → (lty : def Y y ) → 126 onto-iso : {y : Ordinal } → (lty : def Y y ) →
136 func←od {X} {Y} {xmap} xfunc ( func←od yfunc y ) ≡ y 127 od→func {X} {Y} {xmap} xfunc ( od→func yfunc y ) ≡ y
137 128
138 open Onto 129 open Onto
139 130
140 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 131 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
141 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 132 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
151 zmap = {!!} 142 zmap = {!!}
152 xfunc1 : def (Func X Z) xmap1 143 xfunc1 : def (Func X Z) xmap1
153 xfunc1 = {!!} 144 xfunc1 = {!!}
154 zfunc : def (Func Z X) zmap 145 zfunc : def (Func Z X) zmap
155 zfunc = {!!} 146 zfunc = {!!}
156 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od xfunc1 ( func←od zfunc z ) ≡ z 147 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → od→func xfunc1 ( od→func zfunc z ) ≡ z
157 onto-iso1 = {!!} 148 onto-iso1 = {!!}
158 149
159 150
160 record Cardinal (X : OD ) : Set n where 151 record Cardinal (X : OD ) : Set n where
161 field 152 field