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

comparison src/zorn.agda @ 637:c17d46ecb051

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, 21 Jun 2022 11:21:27 +0900
parents 844eb13a5a39
children 75578f19ed3c
comparison
equal deleted inserted replaced
636:844eb13a5a39 637:c17d46ecb051
680 postulate 680 postulate
681 TFcomm : { ψ : Ordinal → Set (Level.suc n) } 681 TFcomm : { ψ : Ordinal → Set (Level.suc n) }
682 → (ind : (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x ) 682 → (ind : (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x )
683 → ∀ (x : Ordinal) → ind x (λ y _ → TransFinite ind y ) ≡ TransFinite ind x 683 → ∀ (x : Ordinal) → ind x (λ y _ → TransFinite ind y ) ≡ TransFinite ind x
684 684
685 record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 685 record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) : Set (Level.suc n) where
686 field 686 field
687 zc : ZChain A y f z 687 zc : ZChain A y f (& A)
688 supf = ZChain.supf zc 688 supf = ZChain.supf zc
689 field 689 field
690 chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z → supf x ⊆' supf y 690 chain-mono : {x y : Ordinal} → x o≤ y → supf x ⊆' supf y
691 f-total : {x : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 691 f-total : {x : Ordinal} → IsTotalOrderSet (supf x)
692 692
693 SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y) 693 SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
694 → (z : Ordinal) → ZChain1 f mf ay z 694 → ZChain1 f mf ay
695 SZ1 f mf {y} ay z = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) z 695 SZ1 f mf {y} ay = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A)
696 ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where 696 ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
697 sf : Ordinal → HOD 697 sf : Ordinal → HOD
698 sf x = ZChain.supf (TransFinite (ind f mf ay) z) x 698 sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x
699 mono : {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → w o≤ z → sf x ⊆' sf w 699 mono : {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w
700 mono {a} {b} sf a≤b b≤z = TransFinite0 {λ b → a o≤ b → b o≤ z → sf a ⊆' sf b } {!!} b a≤b b≤z 700 mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where
701 mind : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x
702 mind = {!!}
703
701 704
702 zorn00 : Maximal A 705 zorn00 : Maximal A
703 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 706 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
704 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where 707 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where
705 -- yes we have the maximal 708 -- yes we have the maximal
714 nmx : ¬ Maximal A 717 nmx : ¬ Maximal A
715 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where 718 nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where
716 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 719 zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y))
717 zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ 720 zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
718 zorn04 : ZChain A (& s) (cf nmx) (& A) 721 zorn04 : ZChain A (& s) (cf nmx) (& A)
719 zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) (& A)) 722 zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) )
720 total : IsTotalOrderSet (ZChain.chain zorn04) 723 total : IsTotalOrderSet (ZChain.chain zorn04)
721 total = ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)) o≤-refl 724 total = ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) )
722 725
723 -- usage (see filter.agda ) 726 -- usage (see filter.agda )
724 -- 727 --
725 -- _⊆'_ : ( A B : HOD ) → Set n 728 -- _⊆'_ : ( A B : HOD ) → Set n
726 -- _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x 729 -- _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x