{-# 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 : HOD) → Set (Level.suc n) x ≤ y = ( x ≡ y ) ∨ ( x < y ) ≤-ftrans : {x y z : HOD} → x ≤ y → y ≤ z → x ≤ z ≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl ≤-ftrans {x} {y} {z} (case1 refl ) (case2 y ¬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 )) x ¬a ¬b c = ⊥-elim z17 where z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) z15 = SUP.x ¬c (λ eq → ¬b (sym eq)) a ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq)) ¬a scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb) scnext : {a : Ordinal} → odef schain a → odef schain (f a) scnext {x} (case1 zx) = case1 (ZChain.f-next zc0 zx) scnext {x} (case2 sx) = case2 ( fsuc x sx ) scinit : {x : Ordinal} → odef schain x → * y ≤ * x scinit {x} (case1 zx) = ZChain.initial zc0 zx scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x