Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 252:8a58e2cd1f55
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 |