# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668378918 -32400
# Node ID 9a85233384f7edc325018fece9623a70b40f211a
# Parent  c8c60a05b39b72ead721dd83d8297c9c13c6c40b
is-max and supf b = supf x

diff -r c8c60a05b39b -r 9a85233384f7 src/zorn.agda
--- a/src/zorn.agda	Sun Nov 13 10:23:50 2022 +0900
+++ b/src/zorn.agda	Mon Nov 14 07:35:18 2022 +0900
@@ -524,7 +524,7 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → supf b o< supf z  → (ab : odef A b)
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
           → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
       order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -645,7 +645,7 @@
 
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-     SZ1 f mf {y} ay zc x = zc1 x where
+     SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
@@ -692,63 +692,63 @@
           ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
           ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
 
-        zc1 :  (x : Ordinal) → ZChain1 A f mf ay zc x
-        zc1 x with Oprev-p x  -- prev is not used now....
+        zc1 :   (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain1 A f mf ay zc y) → ZChain1 A f mf ay zc x
+        zc1 x prev with Oprev-p x  
         ... | yes op = record { is-max = is-max ; order = order  } where
-           px = Oprev.oprev op
-           zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
-           zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
-           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
-              * a < * b → odef (UnionCF A f mf ay supf x) b
-           is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
-           is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup
-             = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
-              b<A : b o< & A
-              b<A = z09 ab
-              b<x : b o< x
-              b<x  = ZChain.supf-inject zc sb<sx
-              m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
-                    chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
-              m05 : ZChain.supf zc b ≡ b
-              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
-              m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-              m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
-              m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
+               px = Oprev.oprev op
+               zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
+               zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) (ZChain.supf-inject zc lt  )
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+                  b o< x → (ab : odef A b) →
+                  HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
+                  * a < * b → odef (UnionCF A f mf ay supf x) b
+               is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
+               is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup
+                 = ⟪ ab , ch-is-sup b sb<sx  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
+                  b<A : b o< & A
+                  b<A = z09 ab
+                  sb<sx : supf b o< supf x
+                  sb<sx  = ? 
+                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                  m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
+                        chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
+                  m05 : ZChain.supf zc b ≡ b
+                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
+                  m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
+                  m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
+                  m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
+                               → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
+                  m09 {s} {z} s<b fcz = order b<A s<b fcz
+                  m06 : ChainP A f mf ay supf b
+                  m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+        ... | no lim = record { is-max = is-max ; order = order }  where
+               is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
+                  b o< x → (ab : odef A b) →
+                  HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
+                  * a < * b → odef (UnionCF A f mf ay supf x) b
+               is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
+               is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
+               is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
+               ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
+               ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
+                  m09 : b o< & A
+                  m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
+                  sb<sx : supf b o< supf x
+                  sb<sx  = ?
+                  m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
+                  m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
+                  m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m09 {s} {z} s<b fcz = order b<A s<b fcz
-              m06 : ChainP A f mf ay supf b
-              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
-        ... | no lim = record { is-max = is-max ; order = order }  where
-           is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              ZChain.supf zc b o< ZChain.supf zc x → (ab : odef A b) →
-              HasPrev A (UnionCF A f mf ay supf x) f b  ∨ IsSUP A (UnionCF A f mf ay supf b) ab →
-              * a < * b → odef (UnionCF A f mf ay supf x) b
-           is-max {a} {b} ua sb<sx ab P a<b with ODC.or-exclude O P
-           is-max {a} {b} ua sb<sx ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b
-           is-max {a} {b} ua sb<sx ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (init-uchain A f mf ay )
-           ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
-              m09 : b o< & A
-              m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-              b<x : b o< x
-              b<x  = ZChain.supf-inject zc sb<sx
-              m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-              m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
-              m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b
-                       → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
-              m08 {s} {z1} s<b fc = order m09 s<b fc
-              m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
-              m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
-                      chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
-                 ; x=fy = HasPrev.x=fy nhp } )
-              m05 : ZChain.supf zc b ≡ b
-              m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
-              m06 : ChainP A f mf ay supf b
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
+                  m08 {s} {z1} s<b fc = order m09 s<b fc
+                  m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) f b
+                  m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
+                          chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp)
+                     ; x=fy = HasPrev.x=fy nhp } )
+                  m05 : ZChain.supf zc b ≡ b
+                  m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
+                  m06 : ChainP A f mf ay supf b
+                  m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -1331,16 +1331,15 @@
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
-            → (ssp<as :  ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
-     fixpoint f mf zc sp1 ssp<as = z14 where
+     fixpoint f mf zc sp1 = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
            sp : Ordinal
            sp = MinSUP.sup sp1
            asp : odef A sp
            asp = MinSUP.asm sp1
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b )
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
@@ -1349,7 +1348,7 @@
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )
@@ -1398,7 +1397,7 @@
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
            (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  msp1 ))))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.asm msp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ss<sa ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ))) -- x ≡ f x ̄
                 (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where          -- x < f x
 
           supf = ZChain.supf zc
@@ -1406,48 +1405,6 @@
           msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
           c : Ordinal
           c = MinSUP.sup msp1
-          c<A : c o< & A
-          c<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
-          asc : odef A (supf c)
-          asc = ZChain.asupf zc
-
-          spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )
-          spd = ysup (cf nmx)  (cf-is-≤-monotonic nmx) asc
-          d = MinSUP.sup spd
-          d<A : d o< & A
-          d<A =  ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
-          msup : MinSUP  A (UnionCF A (cf nmx)  (cf-is-≤-monotonic nmx) as0 supf d)
-          msup = ZChain.minsup zc (o<→≤ d<A)
-          sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
-          sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
-
-          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 with MinSUP.x≤sup spd (init asc refl)
-          ... | case1 eq = ?
-          ... | case2 lt = ?
-
-          ss<sa : supf c o< supf (& A)
-          ss<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ c<A))
-          ... | case2 sc<sa = sc<sa
-          ... | case1 sc=sa = ⊥-elim (  nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd) 
-                ; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where 
-             zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x  → ¬ ( d << x )
-             zc10 = ? where 
-                  zc11 : {z : Ordinal } →  odef (ZChain.chain zc) z → supf z o< supf (& A) 
-                  zc11 = ?
-                  sc≤c : c o≤ supf c 
-                  sc≤c = MinSUP.minsup msp1 ? ?
-                  sc=c : supf c ≡ c
-                  sc=c = ?
-                  d≤c : c o≤ d
-                  d≤c = MinSUP.minsup msp1 ? ?
-                    --    supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
-                    --      c << x → x is sup of chain or x = f ( .. ( f c ))
-                    --      c o≤ x (by minimulity)
-                    --  odef chain z → supf z o< supf (& A) ≡ supf c → supf c is sup of chain, by minimulity  c o≤ supf c 
-                    --   supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A)
-                    --   supf c ≡ supf (supf c) ≡ supf x  ≡ supf (& A)  means supf of FClosure of (supf c) is Maximal
 
      zorn00 : Maximal A
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM