# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655768786 -32400
# Node ID 6cd4a483122c8fc7eddf026b307c14298656e522
# Parent  1b57a07d76046804362ae0994b0127e3dc28fb21
ZChain1 is not strictly positive

diff -r 1b57a07d7604 -r 6cd4a483122c src/zorn.agda
--- a/src/zorn.agda	Mon Jun 20 18:47:37 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 08:46:26 2022 +0900
@@ -247,13 +247,6 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
 
---      chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
---      f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
-
-ZChainSupUnique : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) ( a b : Ordinal )
-   → ( za : ZChain A x f a ) → (zb : ZChain A x f b ) → {i : Ordinal } → a o< b → i o≤ a → ZChain.supf za i ≡ ZChain.supf zb i
-ZChainSupUnique = {!!}
-
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -325,13 +318,8 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (& A) ) → SUP A  (ZChain.chain zc) 
-     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!}   
-     A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx)  (& A) ) 
-        →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )))
-     A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) ) → SUP A (ZChain.chain zc)
-     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!}   
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
+     sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
@@ -339,11 +327,11 @@
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) )
-            → ( {x y : Ordinal} → x o≤ (& A) → IsTotalOrderSet (ZChain.chain zc) )
-            → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
+            → (total : IsTotalOrderSet (ZChain.chain zc) )
+            → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc  total))
      fixpoint f mf zc total = z14 where
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc
+           sp1 = sp0 f mf zc total
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
               →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
@@ -366,8 +354,8 @@
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
-           z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with total {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           z14 :  f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total ))
+           z14 with total (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
@@ -387,12 +375,13 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
-     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ({x y : Ordinal} → x o≤ & A → IsTotalOrderSet (ZChain.chain zc)) → ⊥
-     z04 nmx zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
+     z04 nmx zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
-           (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where          -- x < f x
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
+           (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where          -- x < f x
+          sp1 : SUP A (ZChain.chain zc)
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
           c = & (SUP.sup sp1)
 
      --
@@ -690,27 +679,32 @@
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) (& A)
 
-     ind-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) { y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → (prev : (z : Ordinal) → z o< x → ZChain A y f z) 
-         → (z : Ordinal) → (z<x : z o< x) → ZChain.chain  (prev z z<x )  ⊆'  ZChain.chain ( ind f mf ay x prev )
-     ind-mono f mf ay x prev z z<x = {!!}
-
      postulate
        TFcomm :  { ψ : Ordinal  → Set (Level.suc n) }
           → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
 
-     SZ-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y) 
-         → {a b : Ordinal } → a o< b →
-         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) a )  ⊆' 
-         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b )
-     SZ-mono f mf {y} ay {a} {b} a<b = TransFinite0 {λ b → a o< b →  ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) a )  ⊆'
-         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b ) } szind b a<b where
-          szind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o< y₁ →
-             ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) y₁)) →
-            a o< x → ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) x)
-          szind = {!!}  --
+     record ZChain1 (supf : (z : Ordinal ) → HOD ) ( z : Ordinal ) : Set (Level.suc n) where
+      field
+         chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
+         f-total : {x : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
 
+     SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
+         → (z : Ordinal) → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) z
+     SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) w} indp z where
+         indp :  (x : Ordinal) →
+            ((y₁ : Ordinal) → y₁ o< x → ZChain1 (λ y₂ → ZChain.chain (TransFinite (ind f mf ay) y₂)) y₁) →
+            ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
+         indp x prev with Oprev-p x
+         ... | yes op  = sz02 where
+             sz02 : ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
+             sz02 with ODC.∋-p O A (* x)
+             ... | no noax = {!!}
+             ... | yes noax = {!!}
+         ... | no  ¬ox  with trio< x y
+         ... | tri< a ¬b ¬c = {!!}
+         ... | tri≈ ¬a b ¬c = {!!}
+         ... | tri> ¬a ¬b y<x = {!!}
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -722,7 +716,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 zorn04 {!!} ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 zc1 ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
@@ -730,6 +724,7 @@
               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) ) ⟫
          zorn04 : ZChain A (& s) (cf nmx) (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
+         zc1 =  (ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)) o≤-refl )
 
 -- usage (see filter.agda )
 --