Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 254:2ea2a19f9cd6
ordered pair clean up
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Aug 2019 16:16:51 +0900 |
parents | d09437fcfc7c |
children | 53b7acd63481 |
comparison
equal
deleted
inserted
replaced
253:0446b6c5e7bc | 254:2ea2a19f9cd6 |
---|---|
169 is-o∅ x with trio< x o∅ | 169 is-o∅ x with trio< x o∅ |
170 is-o∅ x | tri< a ¬b ¬c = no ¬b | 170 is-o∅ x | tri< a ¬b ¬c = no ¬b |
171 is-o∅ x | tri≈ ¬a b ¬c = yes b | 171 is-o∅ x | tri≈ ¬a b ¬c = yes b |
172 is-o∅ x | tri> ¬a ¬b c = no ¬b | 172 is-o∅ x | tri> ¬a ¬b c = no ¬b |
173 | 173 |
174 _,_ : OD → OD → OD | |
175 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) | |
176 <_,_> : (x y : OD) → OD | |
177 < x , y > = (x , x ) , (x , y ) | |
178 | |
179 exg-pair : { x y : OD } → (x , y ) == ( y , x ) | |
180 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where | |
181 left : {z : Ordinal} → def (x , y) z → def (y , x) z | |
182 left (case1 t) = case2 t | |
183 left (case2 t) = case1 t | |
184 right : {z : Ordinal} → def (y , x) z → def (x , y) z | |
185 right (case1 t) = case2 t | |
186 right (case2 t) = case1 t | |
187 | |
188 ==-trans : { x y z : OD } → x == y → y == z → x == z | |
189 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } | |
190 | |
191 ==-sym : { x y : OD } → x == y → y == x | |
192 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } | |
193 | |
194 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y | |
195 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) | |
196 | |
197 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y | |
198 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) | |
199 | |
200 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > | |
201 eq-prod refl refl = refl | |
202 | |
203 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) | |
204 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where | |
205 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y | |
206 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) | |
207 lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) | |
208 lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) | |
209 lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) | |
210 lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b | |
211 lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) | |
212 lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) | |
213 lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) | |
214 lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y | |
215 lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where | |
216 lemma3 : ( x , x ) == ( y , z ) | |
217 lemma3 = ==-trans eq exg-pair | |
218 lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y | |
219 lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) | |
220 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) | |
221 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) | |
222 lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z | |
223 lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) | |
224 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z | |
225 ... | refl with lemma2 (==-sym eq ) | |
226 ... | refl = refl | |
227 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z | |
228 lemmax : x ≡ x' | |
229 lemmax with eq→ eq {od→ord (x , x)} (case1 refl) | |
230 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') | |
231 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' | |
232 ... | refl = lemma1 (ord→== s ) | |
233 lemmay : y ≡ y' | |
234 lemmay with lemmax | |
235 ... | refl with lemma4 eq -- with (x,y)≡(x,y') | |
236 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) | |
237 | |
174 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p | 238 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p |
175 ppp {p} {a} d = d | 239 ppp {p} {a} d = d |
176 | 240 |
177 -- | 241 -- |
178 -- Axiom of choice in intutionistic logic implies the exclude middle | 242 -- Axiom of choice in intutionistic logic implies the exclude middle |
266 ZFSet = OD | 330 ZFSet = OD |
267 Select : (X : OD ) → ((x : OD ) → Set n ) → OD | 331 Select : (X : OD ) → ((x : OD ) → Set n ) → OD |
268 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } | 332 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } |
269 Replace : OD → (OD → OD ) → OD | 333 Replace : OD → (OD → OD ) → OD |
270 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } | 334 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } |
271 _,_ : OD → OD → OD | |
272 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) | |
273 _∩_ : ( A B : ZFSet ) → ZFSet | 335 _∩_ : ( A B : ZFSet ) → ZFSet |
274 A ∩ B = record { def = λ x → def A x ∧ def B x } | 336 A ∩ B = record { def = λ x → def A x ∧ def B x } |
275 Union : OD → OD | 337 Union : OD → OD |
276 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } | 338 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } |
277 _∈_ : ( A B : ZFSet ) → Set n | 339 _∈_ : ( A B : ZFSet ) → Set n |
531 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | 593 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) |
532 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | 594 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) |
533 } | 595 } |
534 | 596 |
535 | 597 |
536 _,_ = ZF._,_ OD→ZF | |
537 Union = ZF.Union OD→ZF | 598 Union = ZF.Union OD→ZF |
538 Power = ZF.Power OD→ZF | 599 Power = ZF.Power OD→ZF |
539 Select = ZF.Select OD→ZF | 600 Select = ZF.Select OD→ZF |
540 Replace = ZF.Replace OD→ZF | 601 Replace = ZF.Replace OD→ZF |
541 isZF = ZF.isZF OD→ZF | 602 isZF = ZF.isZF OD→ZF |