# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666553441 -32400
# Node ID 307ad8807963549f8ca0e52fc096b7e55ee64747
# Parent  0e0608b1953bb458a491e05e252e33b435c1a1c5
...

diff -r 0e0608b1953b -r 307ad8807963 src/zorn1.agda
--- a/src/zorn1.agda	Sun Oct 23 23:29:30 2022 +0900
+++ b/src/zorn1.agda	Mon Oct 24 04:30:41 2022 +0900
@@ -653,15 +653,20 @@
          → SUP A (UnionZF f mf ay supf )
      usp0 f mf ay supf  = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf )
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+     msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → (zc : ZChain A f mf ay x ) 
-         → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
-     sp0 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
+         → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
+     msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
         ztotal : IsTotalOrderSet (ZChain.chain zc) 
         ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         → (zc : ZChain A f mf ay x ) 
+         → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
+     sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
+
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A)
             → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
@@ -680,12 +685,16 @@
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
           supf = ZChain.supf zc
+          msp1 : MinSUP A (ZChain.chain zc)
+          msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
           sp1 : SUP A (ZChain.chain zc)
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
-          c = & (SUP.sup sp1)
-          z20 : c << cf nmx c 
-          z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) )
-          asc : odef A (supf c)
+          c : Ordinal 
+          c = & ( SUP.sup sp1 )
+          mc = MinSUP.sup msp1
+          z20 : mc << cf nmx mc 
+          z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) )
+          asc : odef A (supf mc)
           asc = ZChain.asupf zc
           spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) 
           spd = ysup (cf nmx)  (cf-is-≤-monotonic nmx) asc
@@ -724,18 +733,23 @@
                -- z25  (fsuc x lt) = ?        -- cf (sup c) 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
-          sc<sd : supf c << supf d
-          sc<sd = ? 
+          sc<<sd : supf mc << supf d
+          sc<<sd = ? 
               -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
-          -- sco<d : supf c o< supf d
-          -- sco<d with osuc-≡< ( ZChain.supf-<= zc (case2 sc<sd ) )
-          -- ... | case1 eq = ⊥-elim ( <-irr eq sc<sd )
-          -- ... | case2 lt = lt
+          sc<sd : supf mc o< supf d
+          sc<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
+          -- ... | case1 eq = ⊥-elim ( <-irr (case1 (subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq) )) sc<<sd )
+          ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) eq)) sc<<sd )
+          ... | case2 lt = lt
+
+          sms<sa : supf mc o< supf (& A)
+          sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
+          ... | case2 lt = lt
+          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ sc<sd ( ZChain.supf-mono zc (o<→≤ d<A ))))
 
           ss<sa : supf c o< supf (& A)
-          ss<sa = ? -- with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ SUP.as sp0 , lift true ⟫) ))
-          -- ... | case2 lt = lt
-          -- ... | case1 eq = ? -- where
+          ss<sa = ?
+
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where