# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656295916 -32400
# Node ID 3821048a85524735d017e21dd4dd657da8a90447
# Parent  7629714b4d07db236ccc5b9892293c25d338afe5
...

diff -r 7629714b4d07 -r 3821048a8552 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Mon Jun 27 08:01:11 2022 +0900
+++ b/src/OrdUtil.agda	Mon Jun 27 11:11:56 2022 +0900
@@ -76,6 +76,12 @@
 _o≤_ :  Ordinal → Ordinal → Set  n
 a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
+o<→≤ : {a b : Ordinal} → a o< b → a o≤ b
+o<→≤ {a} {b} lt with trio< a (osuc b)
+... | tri< a₁ ¬b ¬c = a₁
+... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) )
+... | tri> ¬a ¬b c  = ⊥-elim (¬a (ordtrans lt <-osuc ) )
+
 -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
 
 xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
diff -r 7629714b4d07 -r 3821048a8552 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 27 08:01:11 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 11:11:56 2022 +0900
@@ -529,6 +529,7 @@
      ... | no ¬ox = record { chain⊆A = Uz⊆A ; f-next = u-next ; chain = Uz
                      ; initial = u-initial ; chain∋x  = u-chain∋x ; is-max = {!!} }   where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
+            inductive
             field
                u : Ordinal
                u<x : u o< x
@@ -551,10 +552,11 @@
          u-chain∋x = case2 ( init ay )
          
      record ZChain1 (y : Ordinal) ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
+      inductive
       field
-         zc : { x : Ordinal } → x o< z → HOD
-         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y<z : y o< z ) →  zc {x} (ordtrans≤-< x≤y y<z)  ⊆' zc y<z  
-         f-total : {x : Ordinal} → (x<z : x o< z ) → IsTotalOrderSet (zc x<z ) 
+         zc : { x : Ordinal } → x o≤ z → ZChain A y f x
+         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y≤z : y o≤ z ) →  ZChain.chain (zc {x} (OrdTrans x≤y y≤z))  ⊆' ZChain.chain (zc y≤z ) 
+         f-total : {x : Ordinal} → (x≤z : x o≤ z ) → IsTotalOrderSet (ZChain.chain (zc x≤z ))
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
          → (z : Ordinal) → ZChain1 y f z
@@ -565,20 +567,22 @@
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
              px = Oprev.oprev op
-             zc1 : ZChain1 y f (Oprev.oprev op)
+             zc1 : ZChain1 y f px
              zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
+             zc0 : ZChain A y f px
+             zc0 = ind f mf ay px (λ w w<px → zc zc1 (o<→≤ w<px) )
              px<x : px o< x
              px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
              sz02 : ZChain1 y f x
              sz02 with ODC.∋-p O A (* x)
              ... | no noax = record { zc = ? ;  chain-mono = ? ; f-total = ? }
-             ... | yes ax with ODC.p∨¬p O ( HasPrev A (zc zc1 ? ) ax f ) 
+             ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f ) 
              ... | case1 pr = record { zc = ? ;  chain-mono = ? ; f-total = ? } where
-             ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (zc zc1 ? ) ax )
+             ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax )
              ... | case1 is-sup = ? where -- x is a sup of zc 1
-                sup0 : SUP A (zc zc1 ? ) 
+                sup0 : SUP A (chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → (zc zc1 ?) ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 :  {y : HOD} → (chain zc0) ∋ y → (y ≡ * x) ∨ (y < * x)
                         x21 {y} zy with IsSup.x<sup is-sup zy 
                         ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k  ) *iso &iso ( cong (*) y=x)  )
                         ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
@@ -586,7 +590,7 @@
                 sp = SUP.sup sup0 
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
-                chain0 = zc zc1 ?
+                chain0 = chain zc0
                 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
                 sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ? )
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
@@ -598,9 +602,6 @@
          ... | tri≈ ¬a b ¬c = {!!}
          ... | tri> ¬a ¬b y<x = {!!}
 
-     zc1=zc : { f : Ordinal → Ordinal } {y : Ordinal} →  ZChain1  y f (osuc (& A)) → ZChain A y f (& A)
-     zc1=zc = ?
-
      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)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
@@ -611,14 +612,14 @@
          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 (zc1=zc zc0) (ZChain1.f-total zc0 <-osuc) ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (ZChain1.zc zc0 o≤-refl ) (ZChain1.f-total zc0 o≤-refl ) ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
-         zc0 : ZChain1 (& s) (cf nmx)  (osuc (& A))
-         zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (osuc (& A))
+         zc0 : ZChain1 (& s) (cf nmx)  (& A)
+         zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)
 
 -- usage (see filter.agda )
 --