# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651136213 -32400
# Node ID 9f24214f4270d00d4abd38ec5782441613c58c83
# Parent  e1a33b1bc16cc720295ae89409a9b8c281424cc3
...

diff -r e1a33b1bc16c -r 9f24214f4270 src/zorn.agda
--- a/src/zorn.agda	Thu Apr 28 12:02:10 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 17:56:53 2022 +0900
@@ -170,11 +170,9 @@
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
-record Indirect< (A : HOD) {x y : Ordinal } (xa : odef A x) (ya : odef A y) (z : Ordinal)  : Set n where
-   field
-      az : odef A z
-      x<z : * x < * z 
-      z<y : * z < * y 
+data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
+   init : {x : Ordinal} → odef A s → FClosure A f s s
+   fsuc : {x : Ordinal} ( p :  FClosure A f s x ) → FClosure A f s (f x)
 
 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
@@ -337,14 +335,71 @@
           zc0 : ZChain A ay f mf supO (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc4 : ZChain A ay f mf supO x 
-          zc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
-          ... | yes ax with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO px
+          zc4 with ODC.∋-p O A (* px)
+          ... | no noapx = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
+                zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                    Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (* (& (ZChain.chain zc0)))
+                       (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
+                       (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)))) ≡ b) →
+                            * a < * b → odef (ZChain.chain zc0) b
+                zc11 {a} {b} za b<x ba P a<b with osuc-≡< (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x) 
+                ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso) ) ba ))
+                ... | case2 lt = ZChain.is-max zc0 za lt ba P a<b
+          ... | yes apx with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO px
           ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+                chain = ZChain.chain zc0
+                zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< x → (ba : odef A b) →
+                            Prev< A (ZChain.chain zc0) ba f ∨ (supO (& (ZChain.chain zc0))
+                             (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
+                             (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) →
+                            * a < * b → odef (ZChain.chain zc0) b
+                zc17 {a} {b} za b<x ba P a<b with osuc-≡< (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x) 
+                ... | case2 lt = ZChain.is-max zc0 za lt ba P a<b
+                ... | case1 b=px = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=px))) ( ZChain.f-next zc0 (Prev<.ay pr))
                 zc9 :  ZChain A ay f mf supO x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
+          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
+          ... | case1 x=sup = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
+                     ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} } where -- x is sup
+                sp = SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) 
+                chain = ZChain.chain zc0
+                z20 : HOD
+                z20 = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} }
+
+          ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
+                     ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+     ... | no ¬ox with trio< (& A) x   --- limit ordinal case
+     ... | tri< a ¬b ¬c = {!!} where
+          zc0 = prev (& A) a
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b c =  {!!} where
+         uzc : HOD
+         uzc = UZFChain f mf x prev
+     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
+         -- yes we have the maximal
+         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
+         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
+         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
+         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 zorn04) 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) ) ⟫
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A ya f mf supO (& A)
+         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A ya f mf supO z } (ind f mf) (& A)
+         zorn04 : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)
+         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso sa )
+
+         zorn99 :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) → (x y : Ordinal) (ay : odef A y) → (zc0 : ZChain A {!!} f mf supO x)  →  Prev< A (ZChain.chain zc0) {!!} f →  {!!}
+         zorn99 f mf x y ay zc0 pr = {!!} where
                 ay0 : odef A (& (* y))
                 ay0 = (subst (λ k → odef A k ) (sym &iso) ay )
                 Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x)
@@ -395,38 +450,6 @@
                     zc6 : IsTotalOrderSet zc5
                     zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
                         ; compare = cmp }
-          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
-          ... | case1 x=sup = {!!} -- x is sup
-          ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
-                     ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
-     ... | no ¬ox with trio< (& A) x   --- limit ordinal case
-     ... | tri< a ¬b ¬c = {!!} where
-          zc0 = prev (& A) a
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b c =  {!!} where
-         uzc : HOD
-         uzc = UZFChain f mf x prev
-     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
-         -- yes we have the maximal
-         zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
-         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
-         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
-         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 zorn04) 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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A ya f mf supO (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A ya f mf supO z } (ind f mf) (& A)
-         zorn04 : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)
-         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso sa )
-
 -- usage (see filter.agda )
 --
 -- _⊆'_ : ( A B : HOD ) → Set n