--- a/src/zorn1.agda	Mon Oct 24 04:30:41 2022 +0900
+++ b/src/zorn1.agda	Mon Oct 24 06:41:01 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)    ⟫
@@ -648,11 +651,6 @@
              → 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)
@@ -692,6 +690,8 @@
           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)
@@ -731,24 +731,25 @@
                -- 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 mc << supf d
           sc<<sd = ? 
-              -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
-          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 )
+
+          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 ( ZChain.supf-mono zc (o<→≤ d<A ))))
+          ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd sc<<sd ) ( ZChain.supf-mono zc (o<→≤ d<A ))))
 
           ss<sa : supf c o< supf (& A)
-          ss<sa = ?
+          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