# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649222538 -32400
# Node ID ed29002a02b6e018d096b1eb01344742813d7ed2
# Parent  ce4f3f180b8e67513fb0f92f691faecfe8bfdabc
zorn again

diff -r ce4f3f180b8e -r ed29002a02b6 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 06 07:57:37 2022 +0900
+++ b/src/zorn.agda	Wed Apr 06 14:22:18 2022 +0900
@@ -52,7 +52,7 @@
 
 PartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
 PartialOrderSet A _<_ = (a b :  Element A)
-     → (elm a < elm b → (¬ (elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
+     → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
 
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
@@ -74,12 +74,9 @@
 
 record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      B : HOD
-      B⊆A : B ⊆ A 
-      total : TotalOrderSet B _<_
-      fb : {x : HOD } → A ∋ x  → HOD
-      B∋fb : (x : HOD ) → (ax : A ∋ x)  → B ∋ fb ax
-      ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< osuc y → sup < fb as
+      fb : Ordinal → HOD
+      A∋fb : (ox : Ordinal ) → ox o< y  → A ∋ fb ox
+      monotonic : (ox oy : Ordinal ) → ox o< y → ox o< oy → fb ox < fb oy 
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
@@ -103,28 +100,31 @@
          z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b (case1 a=b) b<a = proj1 (proj2 (PO (me  A∋b) (me A∋a)) (sym a=b)) b<a
-     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (PO (me  A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me  A∋b) (me A∋a)) b=a ) b<a ) ⟫
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = {!!}
+       -- proj1 (PO (me  A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me  A∋b) (me A∋a)) b=a ) b<a ) ⟫
      -- ZChain is not compatible with the SUP condition
-     ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
-     ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z (SUP.A∋maximal sp)) (ZChain.B∋fb z  _ (SUP.A∋maximal sp)) (ZChain.¬x≤sup z _  (SUP.A∋maximal sp) z03 )) where
+     B :  (z : ZChain A (& A) _<_ ) → HOD
+     B = {!!}
+     ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
+     ZChain→¬SUP z sp = ⊥-elim {!!} where
          z03 : & (SUP.sup sp) o< osuc (& A)
          z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
-         z02 :  (x : HOD) → ZChain.B z ∋ x → SUP.sup sp < x → ⊥
-         z02 x xe s<x = z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
+         z02 :  (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥
+         z02 x xe s<x = {!!} -- z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
      ind :  HasMaximal =h= od∅
          → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
      ind nomx x prev with Oprev-p x
      ... | yes op with ODC.∋-p O A (* x)
-     ... | no ¬Ax = record  { B = ZChain.B zc1 ; B⊆A =  ZChain.B⊆A  zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = z04 } where
+     ... | no ¬Ax = {!!} where
           -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
           px = Oprev.oprev op
           zc1 : ZChain A px _<_
           zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          z04 :  (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
+          z04 :  {!!} -- (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
           z04 sup as s<x with trio< (& sup) x
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
-          ... | tri< a ¬b ¬c  = ZChain.¬x≤sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
+          ... | tri< a ¬b ¬c  = {!!} -- ZChain.¬x≤sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
           ... | tri> ¬a ¬b c with  osuc-≡< s<x
           ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )  
           ... | case2 lt = ⊥-elim (¬a lt )
@@ -139,45 +139,14 @@
               x-is-maximal m am  =  ¬x<m   where
                  ¬x<m :  ¬ (* x < * m)
                  ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
-          ... | no not = record { B = Bx     --  we have larger element, let's create ZChain
-              ; B⊆A = B⊆A ; total = total ; fb = fb ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
-                 B = ZChain.B zc1 
-                 Bx : HOD
-                 Bx = record { od = record { def = λ y → (x ≡ y) ∨ odef B y } ; odmax = & A ; <odmax = {!!}  }  -- Union (B , x)
-                 B⊆A : Bx ⊆ A
-                 B⊆A = record { incl = λ {y} by → z07 y by  } where
-                     z07 : (y : HOD) → Bx ∋ y → A ∋ y
-                     z07 y (case1 x=y) = subst (λ k → odef A k ) (trans &iso x=y) ax
-                     z07 y (case2 by) = incl (ZChain.B⊆A zc1 ) by
-                 m = ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
-                 p : odef A (& m) ∧ (* x < (* (& m)))
-                 p = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
-                 fb :  {y : HOD} → A ∋ y → HOD
-                 fb {y} ay with trio< (& y) x
-                 ... | tri< a ¬b ¬c = ZChain.fb zc1 ay
-                 ... | tri≈ ¬a b ¬c = m
-                 ... | tri> ¬a ¬b c = od∅
-                 total : TotalOrderSet Bx _<_
-                 total ex ey with is-elm ex | is-elm ey
-                 ... | case1 eq | case1 eq1 = tri≈ {!!} {!!} {!!} 
-                 ... | case1 x | case2 x₁ = tri< {!!} {!!} {!!}  
-                 ... | case2 x | case1 x₁ = {!!}
-                 ... | case2 x | case2 x₁ = ZChain.total zc1 (me x) (me x₁)
+          ... | no not = {!!} where
      ind nomx x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
-     ... | tri< a ¬b ¬c = record { B = ZChain.B zc1
-              ; B⊆A = ZChain.B⊆A zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = {!!} } where
+     ... | tri< a ¬b ¬c = {!!} where
           zc1 : ZChain A (& A) _<_
           zc1 = prev (& A) a 
-     ... | tri≈ ¬a b ¬c = record { B = B
-              ; B⊆A = B⊆A ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
-          B : HOD  -- Union (previous B)
-          B = record { od = record { def = λ y → (y o< x) ∧ ((y<x : y o< x ) → odef (ZChain.B (prev y y<x)) y) } ; odmax = & A ; <odmax = {!!} } 
-          B⊆A : B ⊆ A
-          B⊆A = record { incl = λ {y} bx → incl (ZChain.B⊆A (prev (& y) (proj1 bx))) (proj2 bx (proj1 bx)) } 
+     ... | tri≈ ¬a b ¬c = {!!} where
      ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
      ... | no ¬Ax = {!!} where
-          B : HOD  -- Union (previous B)
-          B = record { od = record { def = λ y → (y o< x) ∧ ((y<x : y o< x ) → odef (ZChain.B (prev y y<x)) y) } ; odmax = & A ; <odmax = {!!} } 
      ... | yes ax with is-o∅ (& (Gtx ax))
      ... | yes nogt = ⊥-elim (no-maximal nomx x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal ⟫ ) where -- no larger element, so it is maximal
               x-is-maximal :  (m : Ordinal) → odef A m → ¬ (* x < * m)
@@ -185,23 +154,20 @@
                  ¬x<m :  ¬ (* x < * m)
                  ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
      ... | no not = {!!} where
-          B : HOD  -- Union (x , previous B)
-          B = record { od = record { def = λ y → (y o< osuc x) ∧ ((y<x : y o< x ) → odef (ZChain.B (prev y y<x)) y) } ; odmax = & A ; <odmax = {!!} } 
      zorn00 : Maximal A _<_
      zorn00 with is-o∅ ( & HasMaximal )
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
          -- yes we have the maximal
-         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
-         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
+         hasm :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
+         hasm =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
          zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
-         zorn01 =  proj1 zorn03
+         zorn01 =  proj1 hasm
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
-         zorn02 {x} ax m<x = ((proj2 zorn03) (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A) (≡o∅→=od∅ ¬Maximal)) ( supP B (ZChain.B⊆A (z (& A) (≡o∅→=od∅ ¬Maximal))) (ZChain.total (z (& A) (≡o∅→=od∅ ¬Maximal))) )) where
+         zorn02 {x} ax m<x = ((proj2 hasm) (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
+     ... | yes ¬Maximal = ⊥-elim {!!} where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          z : (x : Ordinal) → HasMaximal =h= od∅  → ZChain A x _<_ 
          z x nomx = TransFinite (ind nomx) x
-         B = ZChain.B (z (& A) (≡o∅→=od∅ ¬Maximal)  )
 
 _⊆'_ : ( A B : HOD ) → Set n
 _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x