{-# OPTIONS --allow-unsolved-metas #-} open import Level hiding ( suc ; zero ) open import Ordinals open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality import OD module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where -- -- Zorn-lemma : { A : HOD } -- → o∅ o< & A -- → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B ) -- SUP condition -- → Maximal A -- open import zf open import logic -- open import partfunc {n} O open import Relation.Nullary open import Data.Empty import BAlgbra open import Data.Nat hiding ( _<_ ; _≤_ ) open import Data.Nat.Properties open import nat open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom import OrdUtil import ODUtil open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal open Ordinals.IsNext isNext open OrdUtil O open ODUtil O import ODC open _∧_ open _∨_ open Bool open HOD -- -- Partial Order on HOD ( possibly limited in A ) -- _<<_ : (x y : Ordinal ) → Set n -- Set n order x << y = * x < * y POO : IsStrictPartialOrder _≡_ _<<_ POO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ; trans = IsStrictPartialOrder.trans PO ; irrefl = λ x=y x ¬a ¬b c = ⊥-elim ( nat-≤> x ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12 where fc12 : * y < * x fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c fcn-imm : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) fcn-imm {A} s {x} {y} f mf cx cy ⟪ x ¬a ¬b c = ⊥-elim ( nat-≤> y ¬a ¬b c with fc20 c -- ncy < suc ncx ... | case1 y=x = <-irr (case1 ( fcn-inject s mf cy cx y=x )) xb (A : HOD) (b : Ordinal) (p : Ordinal) : Set n where field x2 : Ordinal ax2 : odef A x2 bb : IsSup A (* p) ax2 -- -- sup and its fclosure is in a chain HOD -- chain HOD is sorted by sup as Ordinal and <-ordered -- whole chain is a union of separated Chain -- minimum index is y not ϕ -- record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where field y-init : supf o∅ ≡ y au : odef A u ¬u=fx : {x : Ordinal} → ¬ ( u ≡ f x ) asup : (x : Ordinal) → odef A (supf x) fcy (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01 where ct00 : * b < * (supf xa) ct00 = ChainP.fcy ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04 where ct05 : * b < * (supf xa) ct05 = ChainP.order supa c (ChainP.csupz supb) ct04 : * b < * a ct04 with s≤fc (supf xa) f mf fca ... | case1 eq = subst (λ k → * b < k ) eq ct05 ... | case2 lt = IsStrictPartialOrder.trans POO ct05 lt ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) → {x z : Ordinal } → ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z ) ChainP-next A f mf {y} ay supf {x} {z} cp = ? --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp ; au = ChainP.au cp -- ; fcy ¬a ¬b c = ⊥-elim z17 where z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) z15 = SUP.x ¬a ¬b c = ⊥-elim ( ¬x<0 c ) chain-x ne {z} uz@record { proj1 = az ; proj2 = record { u = u ; u ¬a ¬b c = ⊥-elim ( ¬p ¬a ¬b c = ⊥-elim ( ¬p ¬a ¬b c = ⊥-elim ( ¬p ¬a ¬b c = ⊥-elim ( ¬p ¬a ¬b c = ⊥-elim ( ¬pb , then b is Maximal -- px o< sup (fc u) ∈ pchain contradicts b=sup ( x o< sup x ) z19 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px z19 {z} za@record {proj1 = az ; proj2 = record { u = u ; u ¬a ¬b₁ c = ¬b₁ ... | tri< a₁ ¬b₁ ¬c₁ = ¬b₁ ... | tri≈ ¬a u=px ¬c₁ with IsSup.x ¬a ¬b c = y pchain : HOD pchain = UnionCF A f mf ay psupf0 x ptotal : IsTotalOrderSet pchain ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) pchain⊆A : {y : Ordinal} → odef pchain y → odef A y pchain⊆A {y} ny = proj1 ny pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u ¬a ¬b c = spu uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za)) uzc {a} za with UChain.u