# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664502923 -32400
# Node ID 6222efcf3b043fed48f53f40c129d8dd33fa3220
# Parent  1ec8c0cfc89207555ca35325eef9bedeb3f59bf4
MinSUP

diff -r 1ec8c0cfc892 -r 6222efcf3b04 src/zorn.agda
--- a/src/zorn.agda	Sat Sep 24 10:52:57 2022 +0900
+++ b/src/zorn.agda	Fri Sep 30 10:55:23 2022 +0900
@@ -97,6 +97,10 @@
 open _==_
 open _⊆_
 
+-- <-TransFinite : {A x : HOD} → {P : HOD → Set n} → x ∈ A 
+--     → ({x : HOD} → A ∋ x →  ({y : HOD} → A ∋  y → y < x → P y ) → P x) → P x
+-- <-TransFinite = ?
+
 --
 -- Closure of ≤-monotonic function f has total order
 --
@@ -357,6 +361,19 @@
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
+record MinSUP ( A B : HOD )  : Set n where
+   field
+      sup : Ordinal
+      asm : odef A sup
+      x<sup : {x : Ordinal } → odef B x → (x ≡ sup ) ∨ (x << sup )   
+      minsup : { sup1 : Ordinal } → odef A sup1 
+         →  ( {x : Ordinal  } → odef B x → (x ≡ sup1 ) ∨ (x << sup1 ))  → sup o≤ sup1
+
+z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
+z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
+
+-- M→S  : {A B : HOD} → MinSUP A B → SUP A B
+-- M→S {A} {B} ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = MinSUP.x<sup ms } 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
@@ -368,15 +385,18 @@
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
    field
-      sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
+      supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+      supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
+      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
+   sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x) 
+   sup {x} x≤z = ? -- M→S  (minsup x≤z )
+   field
       sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
            → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
 
-      supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz
-      supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
+      -- supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz
       x≤supfx : z o≤ supf z
 
    chain∋init : odef chain y
@@ -410,19 +430,18 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-   supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
-   supf-idem {x} = ?
-
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
 
+   -- supf-idem : {x : Ordinal } → supf x o≤ z  → supf (supf x) ≡ supf x
+   -- supf-idem {x} sx≤z = sup=u (supf∈A ?) sx≤z ?
+
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
-
    -- ordering is not proved here but in ZChain1 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -452,8 +471,6 @@
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
-     z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
-     z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
      s : HOD
      s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
      as : A ∋ * ( & s  )
@@ -476,6 +493,50 @@
         ¬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) 
 
+     minsupP :  ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → MinSUP A B  
+     minsupP B B⊆A total = m02 where
+         xsup : (sup : Ordinal ) → Set n
+         xsup sup = {w : Ordinal } → odef B w → (w ≡ sup ) ∨ (w << sup )
+         ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
+                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
+         ∀-imply-or  {A} {B} ∀AB with ODC.p∨¬p O ((x : Ordinal ) → A x) -- LEM
+         ∀-imply-or  {A} {B} ∀AB | case1 t = case1 t
+         ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x not )) where
+               lemma : ¬ ((x : Ordinal ) → A x) →  B
+               lemma not with ODC.p∨¬p O B
+               lemma not | case1 b = b
+               lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
+         m00 : (x : Ordinal ) → ( ( z : Ordinal) → z o< x →  ¬ (odef A z ∧ xsup z) ) ∨ MinSUP A B
+         m00 x = TransFinite0 ind x where
+            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( ( w : Ordinal) → w o< z →  ¬ (odef A w ∧ xsup w ))  ∨ MinSUP A B)
+                  → ( ( w : Ordinal) → w o< x →  ¬ (odef A w ∧ xsup w) )  ∨ MinSUP A B
+            ind x prev  =  ∀-imply-or m01 where
+                m01 : (z : Ordinal) → (z o< x → ¬ (odef A z ∧ xsup z)) ∨ MinSUP A B
+                m01 z with trio< z x
+                ... | tri≈ ¬a b ¬c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
+                ... | tri> ¬a ¬b c = case1 ( λ lt →  ⊥-elim ( ¬a lt )  )
+                ... | tri< a ¬b ¬c with prev z a
+                ... | case2 mins = case2 mins
+                ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z)
+                ... | case1 mins = case2 record { sup = z ; asm = proj1 mins ; x<sup = proj2 mins ; minsup = m04 } where
+                  m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1
+                  m04 {s} as lt with trio< z s
+                  ... | tri< a ¬b ¬c = o<→≤ a
+                  ... | tri≈ ¬a b ¬c = o≤-refl0 b
+                  ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫  )
+                ... | case2 notz = case1 (λ _ → notz )
+         m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z)
+         m03 not = ⊥-elim ( not s1 (z09 (SUP.as S)) ⟪ SUP.as S , m05 ⟫ ) where
+             S : SUP A B
+             S = supP B  B⊆A total
+             s1 = & (SUP.sup S)
+             m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 )
+             m05 {w} bw with SUP.x<sup S {* w} (subst (λ k → odef B k) (sym &iso) bw )
+             ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) eq) )
+             ... | case2 lt = case2 ( subst (λ k → _ < k ) (sym *iso) lt )
+         m02 : MinSUP A B 
+         m02 = dont-or (m00 (& A)) m03
+
      -- Uncountable ascending chain by axiom of choice
      cf : ¬ Maximal A → Ordinal → Ordinal
      cf  nmx x with ODC.∋-p O A (* x)
@@ -515,31 +576,6 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
-     x≤sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
-         (zc : ZChain A f mf ay x ) → x o≤ & (SUP.sup (sp0 f mf ay zc))
-     x≤sp0 f mf {x} ay zc with trio< x (& (SUP.sup (sp0 f mf ay zc))) 
-     ... | tri< a ¬b ¬c = o<→≤ a
-     ... | tri≈ ¬a b ¬c = o≤-refl0 b
-     ... | tri> ¬a ¬b sp<sp0 = ? where
-           sp1 :  {z : Ordinal } → z o≤ x  → SUP A (UnionCF A f mf ay (ZChain.supf zc) z)
-           sp1 {z} z≤x = ZChain.sup zc z≤x
-
-     record MinSUP ( A B : HOD ) (z : Ordinal) : Set (Level.suc n) where
-       field
-          sup : HOD
-          asm : A ∋ sup
-          x<sup : {x : HOD} → B ∋ x → (& x)  o< z → (x ≡ sup ) ∨ (x < sup )   
-          minsup : {x sup1 : HOD} → B ∋ x → (& x) o< z  → (x ≡ sup1 ) ∨ (x < sup1 )  → sup ≤ sup1
-
-     msupP : {B : HOD} → MinSUP A B (& A)
-     msupP {B} = tf (& A) where
-         ind :  (x : Ordinal) → ((y : Ordinal) → y o< x → MinSUP A B y) → MinSUP A B x
-         ind x prev = ?
-         tf : (z : Ordinal) → MinSUP A B z
-         tf z = TransFinite {λ x → MinSUP A B x } ind z
-
-     M→S  : {B : HOD} {z : Ordinal } → (& B) o< z  → MinSUP A B z → SUP A B
-     M→S {B} lt ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = ? }
 
      --
      -- Second TransFinite Pass for maximality
@@ -842,7 +878,7 @@
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
-                 ... | tri≈ ¬a b ¬c = px
+                 ... | tri≈ ¬a b ¬c = px   --- supf px ≡ px
                  ... | tri> ¬a ¬b c = sp1 
 
                  pchainp : HOD
@@ -929,9 +965,9 @@
                     ... | case1 eq = ?
                     ... | case2 lt = ?
 
-          ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
-                          ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
-
+          ... | case2 px<spfx = ? where
+            -- record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
+            --              ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
@@ -1136,8 +1172,8 @@
           zc70 pr xsup = ?
 
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u  
-               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
+          no-extension ¬sp=x  = ? where -- record { supf = supf1  ; sup=u = sup=u  
+               -- ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  pchain0=1 : pchain ≡ pchain1
@@ -1185,8 +1221,8 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { supf = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?) 
+          ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!} 
+               -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)