# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655522889 -32400
# Node ID 3938bed729a512346c386084e097f42b8ae3edef
# Parent  e766238b69d23973784b138bfb41e86725ed8038
min-sup

diff -r e766238b69d2 -r 3938bed729a5 src/OD.agda
--- a/src/OD.agda	Sat Jun 18 10:16:19 2022 +0900
+++ b/src/OD.agda	Sat Jun 18 12:28:09 2022 +0900
@@ -99,6 +99,7 @@
   *iso   :  {x : HOD }      → * ( & x ) ≡ x
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
+-- these are valid theorem because of the TransFinite induction (but we leave it now)
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 -- possible order restriction
diff -r e766238b69d2 -r 3938bed729a5 src/zorn.agda
--- a/src/zorn.agda	Sat Jun 18 10:16:19 2022 +0900
+++ b/src/zorn.agda	Sat Jun 18 12:28:09 2022 +0900
@@ -232,6 +232,7 @@
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+      min-sup : {z : Ordinal} → ( {y : Ordinal} → odef B y → (y ≡ z ) ∨ (y << z ) ) → x o≤ z
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -349,7 +350,7 @@
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.A∋maximal sp1)
-               z19 = record {   x<sup = z20 }  where
+               z19 = record {   x<sup = z20 ; min-sup = {!!} }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
                    z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
@@ -376,8 +377,8 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ 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 (& s) (cf nmx)  (& A)) → ⊥
-     z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
+     ¬Maximal→¬ZChain  :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx)  (& A)) → ⊥
+     ¬Maximal→¬ZChain nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where          -- x < f x
@@ -446,7 +447,7 @@
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
-          ... | case1 is-sup = -- x is a sup of zc0 
+          ... | case1 is-sup = -- x is the min sup of zc0 
                 record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
                      ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax } where 
                 sup0 : SUP A (ZChain.chain zc0) 
@@ -536,18 +537,18 @@
                      z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
                 s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (case2 z22) a<b ) where -- previous sup
                      z22 : IsSup A (ZChain.chain zc0)   ab 
-                     z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
+                     z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) ; min-sup = {!!} }
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
-                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))               -- in previous closure of f
+                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))              -- in previous closure of f
                 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy ))  -- in current  closure of f
                 s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc0
                      z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab 
-                     z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
+                     z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) ; min-sup = {!!} }
                      z23 : odef chain0 b
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
-          ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
+          ... | case2 ¬x=sup =  -- x is not f y' nor min-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 = z18 }  where
                       -- no extention
@@ -559,7 +560,7 @@
                 ... | case1 b=x with p
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
-                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  ; min-sup = {!!} } ) 
      ... | no ¬ox with trio< x y
      ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
@@ -643,16 +644,16 @@
          zorn01  = proj1  zorn03  
          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 ( z04 nmx zorn04) where
+     ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬ZChain nmx max-chain-mf) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
-         zorn04 : ZChain A (& s) (cf nmx)  (& A)
-         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
+         max-chain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
+         max-chain f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
+         max-chain-mf : ZChain A (& s) (cf nmx)  (& A)
+         max-chain-mf = max-chain (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
 -- usage (see filter.agda )
 --