# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666571767 -32400
# Node ID ebcad8e5ae557ec56ad3171563243d44a506cd90
# Parent  409ac0af7b3b0fdcb9938538f09c94d49529549d
resync zorn.agda

diff -r 409ac0af7b3b -r ebcad8e5ae55 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 24 09:15:49 2022 +0900
+++ b/src/zorn.agda	Mon Oct 24 09:36:07 2022 +0900
@@ -413,9 +413,12 @@
    chain = UnionCF A f mf ay supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
+
    sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x) 
    sup {x} x≤z = M→S supf (minsup x≤z) 
-   -- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono
+
+   s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z)
+   s=ms {x} x≤z = &iso
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -1331,19 +1334,19 @@
              → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua )
           uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb)
 
-     usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)  
-         → ( supf : Ordinal → Ordinal )
-         → 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 )
+     msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         → (zc : ZChain A f mf ay x ) 
+         → 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 {x} ay zc = supP (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 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)
@@ -1411,12 +1414,18 @@
            (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
+          c=mc : c ≡ mc
+          c=mc = &iso
+          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
@@ -1453,20 +1462,36 @@
                -- z25 : {x : Ordinal } → odef (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )  
                -- z25 {x} (init au eq ) = ?   -- sup c = x, cf y ≡ d, sup c =< d
                -- 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 = ? 
-              -- 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<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+             → supf mc << MinSUP.sup spd
+          sc<<d {mc} {asc} spd = z25 where
+                d1 :  Ordinal
+                d1 = MinSUP.sup spd
+                z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
+                z24 = MinSUP.x<sup spd (init asc refl)
+                z25 : supf mc << d1
+                z25 with z24
+                ... | case2 lt = lt
+                ... | case1 eq = ?
+
+          sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
+          sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
+          ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym 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 (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) ) 
+              ( 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 = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<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