# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651263113 -32400
# Node ID d09f9a1d6c2f93c4441423df5fefd7dbbc9e2c9b
# Parent  9ba98ecfbe626ceafed5dfe5ed07e79e1082fb4f
...

diff -r 9ba98ecfbe62 -r d09f9a1d6c2f src/zorn.agda
--- a/src/zorn.agda	Sat Apr 30 04:41:06 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 05:11:53 2022 +0900
@@ -7,6 +7,13 @@
 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
@@ -43,6 +50,10 @@
 
 open HOD
 
+--
+-- Partial Order on HOD ( possibly limited in A )
+--
+
 _≤_ : (x y : HOD) → Set (Level.suc n)
 x ≤ y = ( x ≡ y ) ∨ ( x < y )
 
@@ -60,28 +71,15 @@
 open _==_
 open _⊆_
 
--- open import Relation.Binary.Properties.Poset as Poset
-
-IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
-IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
-
-      
-record Maximal ( A : HOD )  : Set (Level.suc n) where
-   field
-      maximal : HOD
-      A∋maximal : A ∋ maximal
-      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
-
 --
--- inductive maxmum tree from x
--- tree structure
+-- Closure of ≤-monotonic function f has total order
 --
 
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
-immieate-f : (A : HOD) → ( f : Ordinal → Ordinal )  → Set n
-immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
+-- immieate-f : (A : HOD) → ( f : Ordinal → Ordinal )  → Set n
+-- immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
 
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
    init : odef A s → FClosure A f s s
@@ -121,7 +119,7 @@
      ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where
           fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y)
           fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) )
-          ... | case1 eq = trans (sym eq) ( fc02  x1 cx1 i=x1 )  
+          ... | case1 eq = trans (sym eq) ( fc02  x1 cx1 i=x1 )  -- derefence while f x ≡ x
           ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where
                fc04 : * x1 ≡ * y
                fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
@@ -162,29 +160,22 @@
       fc12 : * y < * x
       fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c
 
--- fcn-cmp {A} s {.s} {.s} f mf (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
--- fcn-cmp {A} s   f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
--- ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
--- ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
---      lt : * s < * (f y)
---      lt with s≤fc  s f mf cy
---      ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
---      ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
--- fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc  s f mf cx 
--- ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
--- ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt)  (λ eq → <-irr (case1 eq) s<x  ) s<x
--- fcn-cmp {A} s   f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
--- ... | case1 x=fx | case1 y=fy = {!!}
--- ... | case1 x=fx | case2 y<fy = {!!}
--- ... | case2 x<fx | case1 y=fy = {!!}
--- ... | case2 x<fx | case2 y<fy = {!!} where
---      fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x
---      fc-mono = {!!}
---      fc1 :  Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x))
---      fc1 with fcn-cmp s f mf imm cx cy
---      ... | tri< a ¬b ¬c = {!!}
---      ... | tri≈ ¬a b ¬c = {!!}
---      ... | tri> ¬a ¬b c = {!!}
+-- open import Relation.Binary.Properties.Poset as Poset
+
+IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
+IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
+
+      
+record Maximal ( A : HOD )  : Set (Level.suc n) where
+   field
+      maximal : HOD
+      A∋maximal : A ∋ maximal
+      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
+
+--
+-- inductive maxmum tree from x
+-- tree structure
+--
 
 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
@@ -247,7 +238,7 @@
         ¬x<m :  ¬ (* x < * m)
         ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
 
-     -- Uncountable acending chain by axiom of choice
+     -- Uncountable ascending chain by axiom of choice
      cf : ¬ Maximal A → Ordinal → Ordinal
      cf  nmx x with ODC.∋-p O A (* x)
      ... | no _ = o∅
@@ -278,7 +269,7 @@
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
      ---
-     --- sup is fix point in maximum chain
+     --- the maximum chain  has fix point of any ≤-monotonic function
      ---
      z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) )
             → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
@@ -315,7 +306,12 @@
                z17 with z15
                ... | case1 eq = ¬b eq
                ... | case2 lt = ¬a lt
-     -- ZChain requires the Maximal
+
+     -- ZChain contradicts ¬ Maximal
+     --
+     -- ZChain forces fix point on any ≤-monotonic function (z03)
+     -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
+     --
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
      z04 nmx zc = z01  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso)
            (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
@@ -324,24 +320,23 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
-     -- 3cases : {x y : Ordinal} → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )
-     --    → (ax : odef A x )→ (ay : odef A y )
-     --    → (zc0 :  ZChain A ay f mf supO x ) 
-     --    →  Prev< A (ZChain.chain zc0) ax f
-     --       ∨  (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x)
-     --       ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x ))
-     -- 3cases {x} {y} f mf ax ay zc0 = {!!}
+     --
      -- create all ZChains under o< x
+     --
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
             ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO x
      ind f mf x prev {y} ay with Oprev-p x
      ... | yes op = zc4 where
+          --
+          -- we have previous ordinal to use induction
+          --
           px = Oprev.oprev op
           zc0 : ZChain A ay f mf supO (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc4 : ZChain A ay f mf supO x 
           zc4 with ODC.∋-p O A (* px)
-          ... | no noapx = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
+          ... | no noapx =  -- ¬ A ∋ px, just skip
+                 record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
                      ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
@@ -367,13 +362,15 @@
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
           ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
-          ... | case1 x=sup = record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
+          ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
+                 record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
                      ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
                 sp = SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) 
                 chain = ZChain.chain zc0
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} }
-          ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
+          ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
+                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
                             Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0)))
@@ -393,6 +390,7 @@
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = {!!} }
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
+         --- ux ⊆ uy ∨ uy ⊆ ux
          
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM