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

comparison OD.agda @ 402:d87492ae4040

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, 28 Jul 2020 10:32:33 +0900
parents 59152f16125a
children ce2ce3f62023
comparison
equal deleted inserted replaced
401:59152f16125a 402:d87492ae4040
386 386
387 Power : HOD → HOD 387 Power : HOD → HOD
388 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) 388 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
389 -- ｛_｝ : ZFSet → ZFSet 389 -- ｛_｝ : ZFSet → ZFSet
390 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly 390 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly
391
392 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
393 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
394 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
395 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
396 union← X z UX∋z = FExists _ lemma UX∋z where
397 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
398 lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx }
391 399
392 data infinite-d : ( x : Ordinal ) → Set n where 400 data infinite-d : ( x : Ordinal ) → Set n where
393 iφ : infinite-d o∅ 401 iφ : infinite-d o∅
394 isuc : {x : Ordinal } → infinite-d x → 402 isuc : {x : Ordinal } → infinite-d x →
395 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 403 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
454 lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl 462 lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
455 463
456 _=h=_ : (x y : HOD) → Set n 464 _=h=_ : (x y : HOD) → Set n
457 x =h= y = od x == od y 465 x =h= y = od x == od y
458 466
467 infixr 200 _∈_
468 -- infixr 230 _∩_ _∪_
469
470 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y )
471 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
472 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))
473
474 pair← : ( x y t : HOD ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t
475 pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
476 pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
477
478 pair1 : { x y : HOD } → (x , y ) ∋ x
479 pair1 = case1 refl
480
481 pair2 : { x y : HOD } → (x , y ) ∋ y
482 pair2 = case2 refl
483
484 empty : (x : HOD ) → ¬ (od∅ ∋ x)
485 empty x = ¬x<0
486
487 o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
488 o<→c< lt = record { incl = λ z → ordtrans z lt }
489
490 ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y
491 ⊆→o< {x} {y} lt with trio< x y
492 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
493 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
494 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl )
495 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
496
459 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 497 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
460 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m 498 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m
461 499
462 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 500 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
463 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where 501 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where
464 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) → 502 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
465 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x 503 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
466 ind {x} prev lt = ind1 lt oiso where 504 ind {x} prev lt = ind1 lt oiso where
467 ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x 505 ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x
468 ind1 {o∅} iφ refl = sym o∅≡od∅ 506 ind1 {o∅} iφ refl = sym o∅≡od∅
469 ind1 {_} (isuc {x₁} ltd) ox=x = begin 507 ind1 (isuc {x₁} ltd) ox=x = begin
470 nat→ω (ω→nato (isuc ltd) ) 508 nat→ω (ω→nato (isuc ltd) )
471 ≡⟨⟩ 509 ≡⟨⟩
472 Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) 510 Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
473 ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ 511 ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩
474 Union (ord→od x₁ , (ord→od x₁ , ord→od x₁)) 512 Union (ord→od x₁ , (ord→od x₁ , ord→od x₁))
475 ≡⟨ trans ( sym oiso) ox=x ⟩ 513 ≡⟨ trans ( sym oiso) ox=x ⟩
476 x 514 x
477 ∎ where 515 ∎ where
478 open ≡-Reasoning 516 open ≡-Reasoning
479 lemma0 : x ∋ ord→od x₁ 517 lemma0 : x ∋ ord→od x₁
480 lemma0 = {!!} 518 lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not
519 (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
481 lemma1 : infinite ∋ ord→od x₁ 520 lemma1 : infinite ∋ ord→od x₁
482 lemma1 = {!!} 521 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
483 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ 522 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁
484 lemma with prev {ord→od x₁} lemma0 lemma1 523 lemma with prev {ord→od x₁} lemma0 lemma1
485 ... | t = {!!} 524 ... | t = {!!}
486
487
488
489 infixr 200 _∈_
490 -- infixr 230 _∩_ _∪_
491
492 pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y )
493 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
494 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))
495
496 pair← : ( x y t : HOD ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t
497 pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
498 pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
499
500 empty : (x : HOD ) → ¬ (od∅ ∋ x)
501 empty x = ¬x<0
502
503 o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
504 o<→c< lt = record { incl = λ z → ordtrans z lt }
505
506 ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y
507 ⊆→o< {x} {y} lt with trio< x y
508 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
509 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
510 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl )
511 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
512
513 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
514 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
515 ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
516 union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
517 union← X z UX∋z = FExists _ lemma UX∋z where
518 lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
519 lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx }
520 525
521 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y 526 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y
522 ψiso {ψ} t refl = t 527 ψiso {ψ} t refl = t
523 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 528 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
524 selection {ψ} {X} {y} = record { 529 selection {ψ} {X} {y} = record {