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

comparison cardinal.agda @ 252:8a58e2cd1f55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up product uniquness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 03:03:04 +0900
parents 9e0125b06e76
children 0446b6c5e7bc
comparison
equal deleted inserted replaced
251:9e0125b06e76 252:8a58e2cd1f55
117 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( 117 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
118 let open ≡-Reasoning in begin 118 let open ≡-Reasoning in begin
119 od→ord < ord→od (od→ord x) , ord→od (od→ord y) > 119 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
120 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ 120 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
121 od→ord < x , y > 121 od→ord < x , y >
122 ∎ ) 122 ∎ )
123 123
124 124
125 lemma44 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) 125 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
126 lemma44 {ox} {oy} = pair ox oy 126 p-iso1 {ox} {oy} = pair ox oy
127 127
128 lemma55 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > 128 postulate
129 lemma55 {ox} {oy} = pair ox oy 129 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
130 130
131 lemma66 : {ox oy : Ordinal } → pair ( pi1 ( pair ox oy )) ( pi2 ( pair ox oy )) ≡ pair ox oy
132 lemma66 = refl
133
134 lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy )) , ord→od (pi2 ( pair ox oy )) > ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
135 lemma77 = refl
136
137
138 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
139 p-iso {x} p = {!!} where
140
141 pair-iso : {op ox oy : Ordinal} (x : ord-pair (od→ord < ord→od ox , ord→od oy >) ) → pi1 x ≡ ox → pi2 x ≡ oy → x ≡ pair ox oy
142 pair-iso (pair ox oy) = {!!}
143
144 p-iso3 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy
145 p-iso3 {ox} {oy} p with p-iso p
146 ... | eq with prod-eq ( ord→== (cong (λ k → od→ord k) eq ) )
147 ... | record { proj1 = eq1 ; proj2 = eq2 } = lemma eq1 eq2 where
148 lemma : ord→od (pi1 p) ≡ ord→od ox → ord→od (pi2 p) ≡ ord→od oy → p ≡ pair ox oy
149 lemma eq1 eq2 with od≡→≡ eq1 | od≡→≡ eq2
150 ... | eq1' | eq2' = pair-iso {od→ord < ord→od ox , ord→od oy >} {ox} {oy} p eq1' eq2'
151
152 p-iso2 : { ox oy : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy
153 p-iso2 {ox} {oy} = p-iso3 (p-cons (ord→od ox) (ord→od oy))
154
155 p-iso1 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ < ord→od ox , ord→od oy >
156 p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p))
157 ... | t with p-iso3 p | p-iso3 t
158 ... | refl | refl = refl
159 131
160 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 132 ∋-p : (A x : OD ) → Dec ( A ∋ x )
161 ∋-p A x with p∨¬p ( A ∋ x ) 133 ∋-p A x with p∨¬p ( A ∋ x )
162 ∋-p A x | case1 t = yes t 134 ∋-p A x | case1 t = yes t
163 ∋-p A x | case2 t = no t 135 ∋-p A x | case2 t = no t