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

comparison OD.agda @ 360:2a8a51375e49

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 Wed, 15 Jul 2020 08:42:30 +0900
parents 811152bf2f47
children 4cbcf71b09c4
comparison
equal deleted inserted replaced
359:5e22b23ee3fd 360:2a8a51375e49
247 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 247 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
248 248
249 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD 249 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
250 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } 250 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
251 251
252 ZFSubset : (A x : HOD ) → HOD 252 _∩_ : ( A B : HOD ) → HOD
253 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set 253 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
254 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) 254 ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
255 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
256 255
257 record _⊆_ ( A B : HOD ) : Set (suc n) where 256 record _⊆_ ( A B : HOD ) : Set (suc n) where
258 field 257 field
259 incl : { x : HOD } → A ∋ x → B ∋ x 258 incl : { x : HOD } → A ∋ x → B ∋ x
260 259
279 y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z 278 y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
280 y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 279 y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x
281 lemma1 : osuc (od→ord y) o< od→ord (x , x) 280 lemma1 : osuc (od→ord y) o< od→ord (x , x)
282 lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) 281 lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c )
283 282
284 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) 283 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A )
285 subset-lemma {A} {x} = record { 284 subset-lemma {A} {x} = record {
286 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } 285 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) }
287 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 286 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
288 } 287 }
289 288
335 ; odmax = rmax ; <odmax = rmax<} where 334 ; odmax = rmax ; <odmax = rmax<} where
336 rmax : Ordinal 335 rmax : Ordinal
337 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) 336 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
338 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax 337 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
339 rmax< lt = proj1 lt 338 rmax< lt = proj1 lt
340 _∩_ : ( A B : ZFSet ) → ZFSet
341 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
342 ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
343 Union : HOD → HOD 339 Union : HOD → HOD
344 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } 340 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) }
345 ; odmax = osuc (od→ord U) ; <odmax = umax< } where 341 ; odmax = osuc (od→ord U) ; <odmax = umax< } where
346 umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) 342 umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
347 umax< {y} not = lemma (FExists _ lemma1 not ) where 343 umax< {y} not = lemma (FExists _ lemma1 not ) where
358 lemma not | tri> ¬a ¬b c = ⊥-elim (not c) 354 lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
359 _∈_ : ( A B : ZFSet ) → Set n 355 _∈_ : ( A B : ZFSet ) → Set n
360 A ∈ B = B ∋ A 356 A ∈ B = B ∋ A
361 357
362 OPwr : (A : HOD ) → HOD 358 OPwr : (A : HOD ) → HOD
363 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) 359 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )
364 360
365 Power : HOD → HOD 361 Power : HOD → HOD
366 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) 362 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
367 -- ｛_｝ : ZFSet → ZFSet 363 -- ｛_｝ : ZFSet → ZFSet
368 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly 364 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly
493 --- 489 ---
494 --- Power Set 490 --- Power Set
495 --- 491 ---
496 --- First consider ordinals in HOD 492 --- First consider ordinals in HOD
497 --- 493 ---
498 --- ZFSubset A x = record { def = λ y → odef A y ∧ odef x y } subset of A 494 --- A ∩ x = record { def = λ y → odef A y ∧ odef x y } subset of A
499 -- 495 --
500 -- 496 --
501 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) 497 ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
502 ∩-≡ {a} {b} inc = record { 498 ∩-≡ {a} {b} inc = record {
503 eq→ = λ {x} x<a → record { proj2 = x<a ; 499 eq→ = λ {x} x<a → record { proj2 = x<a ;
504 proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 500 proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ;
505 eq← = λ {x} x<a∩b → proj2 x<a∩b } 501 eq← = λ {x} x<a∩b → proj2 x<a∩b }
506 -- 502 --
507 -- Transitive Set case 503 -- Transitive Set case
508 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t =h= t 504 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
509 -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t 505 -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
510 -- OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 506 -- OPwr A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) )
511 -- 507 --
512 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t 508 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
513 ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t} 509 ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t}
514 lemma refl (lemma1 lemma-eq )where 510 lemma refl (lemma1 lemma-eq )where
515 lemma-eq : ZFSubset (Ord a) t =h= t 511 lemma-eq : ((Ord a) ∩ t) =h= t
516 eq→ lemma-eq {z} w = proj2 w 512 eq→ lemma-eq {z} w = proj2 w
517 eq← lemma-eq {z} w = record { proj2 = w ; 513 eq← lemma-eq {z} w = record { proj2 = w ;
518 proj1 = odef-subst {_} {_} {(Ord a)} {z} 514 proj1 = odef-subst {_} {_} {(Ord a)} {z}
519 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 515 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
520 lemma1 : {a : Ordinal } { t : HOD } 516 lemma1 : {a : Ordinal } { t : HOD }
521 → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 517 → (eq : ((Ord a) ∩ t) =h= t) → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
522 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 518 lemma1 {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
523 lemma2 : (od→ord t) o< (osuc (od→ord (Ord a))) 519 lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
524 lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 520 lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t)))
525 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x))) 521 lemma : od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
526 lemma = sup-o< _ lemma2 522 lemma = sup-o< _ lemma2
527 523
528 -- 524 --
529 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first 525 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
530 -- then replace of all elements of the Power set by A ∩ y 526 -- then replace of all elements of the Power set by A ∩ y
559 A ∩ t 555 A ∩ t
560 ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ 556 ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
561 t 557 t
562 ∎ 558 ∎
563 sup1 : Ordinal 559 sup1 : Ordinal
564 sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))) 560 sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x)))
565 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) 561 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
566 lemma9 = <-osuc 562 lemma9 = <-osuc
567 lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 563 lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
568 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 564 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9
569 lemmad : Ord (osuc (od→ord A)) ∋ t 565 lemmad : Ord (osuc (od→ord A)) ∋ t
570 lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) 566 lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt)))
571 lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A) 567 lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
572 lemmac = record { eq→ = lemmaf ; eq← = lemmag } where 568 lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
573 lemmaf : {x : Ordinal} → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x 569 lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
574 lemmaf {x} lt = proj1 lt 570 lemmaf {x} lt = proj1 lt
575 lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x 571 lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x
576 lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } 572 lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt }
577 lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) 573 lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
578 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) 574 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
579 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 575 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
580 lemma7 with osuc-≡< lemmad 576 lemma7 with osuc-≡< lemmad
581 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab ) 577 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
582 lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where 578 lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where