# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666306627 -32400
# Node ID 0f2a85826cc7b354d550a803db71890ae723f874
# Parent  4b88d9a98d209385a81aa1256f91bf386c58812f
...

diff -r 4b88d9a98d20 -r 0f2a85826cc7 src/zorn.agda
--- a/src/zorn.agda	Thu Oct 20 09:35:52 2022 +0900
+++ b/src/zorn.agda	Fri Oct 21 07:57:07 2022 +0900
@@ -1318,12 +1318,6 @@
      uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-is-sup u u<x is-sup fc ⟫) with ChainP.supu=u is-sup
      ... | eq = ch-is-sup u u<x is-sup fc 
 
-     zc⊆uzc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → {x ux : Ordinal } → UChain A f mf ay supf ux x → ZChainP f mf ay supf x
-     zc⊆uzc f mf {y} ay supf {x} ( ch-init fc ) = zchain x ⟪ A∋fc y f mf fc ,  ch-init fc ⟫
-     zc⊆uzc f mf {y} ay supf {x} ( ch-is-sup u1 u1<x u1-is-sup fc ) 
-        = zchain ? ⟪ A∋fc (supf u1) f mf fc ,  ch-is-sup u1 ? u1-is-sup fc ⟫
-
      UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
             (supf : Ordinal → Ordinal )  → HOD
      UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } 
@@ -1337,10 +1331,10 @@
              → 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 ) {x y : Ordinal} (ay : odef A y)  
+     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 {x} ay supf  = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal 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)  
          → (zc : ZChain A f mf ay x ) 
@@ -1352,8 +1346,9 @@
                uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
      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  ))
-     fixpoint f mf zc = z14 where
+     fixpoint f mf zc ss<sa = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
            sp1 : SUP A chain
@@ -1365,7 +1360,7 @@
            z22 : & (SUP.sup sp1) o< & A
            z22 = c<→o< ( SUP.as sp1 )
            z21 : supf (& (SUP.sup sp1)) o< supf (& A)
-           z21 = ?
+           z21 = ss<sa
            -- z21 : supf (& (SUP.sup sp1)) o< & A
            -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) ))
            z12 : odef chain (& (SUP.sup sp1))
@@ -1413,11 +1408,20 @@
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
+           (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
           sp1 : SUP A (ZChain.chain zc)
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
           c = & (SUP.sup sp1)
+          d : Ordinal
+          d = cf nmx (supf c )
+          z21 : d o< & A
+          z21 =  ∈∧P→o< ⟪ proj2 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc))  , lift true ⟫
+          z20 : supf c << d
+          z20 = proj1 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc) )
+          ss<sa : supf c o< supf (& A)
+          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
@@ -1428,7 +1432,7 @@
          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 ? ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (SZ (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) )) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where