# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655772312 -32400
# Node ID fd7dc627748079675d0b4412f85b522cb15c7dbf
# Parent  6cd4a483122c8fc7eddf026b307c14298656e522
...

diff -r 6cd4a483122c -r fd7dc6277480 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 21 08:46:26 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 09:45:12 2022 +0900
@@ -246,6 +246,7 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
+      pmono : (x : Ordinal ) → x o≤ z → supf x ⊆' supf z
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -393,7 +394,7 @@
      init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
      init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
                      ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf 
-                     ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max } where
+                     ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max ; pmono = {!!} } where
                i-total : IsTotalOrderSet (ys ay f mf )
                i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
                is-max : {a b : Ordinal} → odef (ys ay f mf) a →
@@ -404,42 +405,47 @@
                initial {i} (init ai) = case1 refl
                initial .{f x} (fsuc x lt) = {!!}
 
+     record ZChain0 ( A : HOD ) : Set (Level.suc n) where
+        field
+           chain : HOD
+           chain⊆A : chain ⊆' A
+
      sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → HOD ) → HOD
+         → ((z : Ordinal) → z o< x → ZChain0 A ) → ZChain0 A
      sind f mf {y} ay x prev  with Oprev-p x
      ... | yes op = sc4 where
           px = Oprev.oprev op
-          sc : HOD
+          sc : ZChain0 A
           sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
 
-          sc4 : HOD
+          sc4 : ZChain0 A
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = {!!}
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A sc ax f )   
+          ... | no noax = sc
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain0.chain sc) ax f )   
           ... | case1 pr = sc
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A sc ax )
-          ... | case1 is-sup =  schain where
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain0.chain sc) ax )
+          ... | case1 is-sup = record { chain =  schain ; chain⊆A = {!!} } where
                 -- A∋sc -- x is a sup of zc 
-                sup0 : SUP A sc 
+                sup0 : SUP A (ZChain0.chain sc )
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → sc ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 :  {y : HOD} → (ZChain0.chain sc) ∋ 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)  )
+                        ... | 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  )
                 sp : HOD
                 sp = SUP.sup sup0 
                 schain : HOD
-                schain = record { od = record { def = λ x → odef sc x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-          ... | case2 ¬x=sup =  sc
+                schain = record { od = record { def = λ x → odef (ZChain0.chain sc) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+          ... | case2 ¬x=sup = sc
      ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = {!!}
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b y<x = Uz where
+     ... | tri< a ¬b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}}  ; chain⊆A = {!!}  }
+     ... | tri≈ ¬a b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}}  ; chain⊆A = {!!}  }
+     ... | tri> ¬a ¬b y<x = record { chain = Uz ; chain⊆A = {!!} } where
          record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x
             field
                u : Ordinal
                u<x : u o< x
-               chain∋z : odef (prev u u<x ) z
+               chain∋z : odef (ZChain0.chain (prev u u<x )) z
          Uz : HOD
          Uz = record { od = record { def = λ y → Usup y } ; odmax = & A
              ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
@@ -470,7 +476,7 @@
           no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc)
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc)
                      ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) 
-                     ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
+                     ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc) ; pmono = {!!} 
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } where
                 supf0 : Ordinal → HOD
@@ -509,7 +515,7 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!} 
+                record {  chain⊆A = {!!} ; f-next = {!!}  ; pmono = {!!}
                      ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -607,8 +613,6 @@
                 ... | tri< a ¬b ¬c = refl
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
-                mono : {a b  : Ordinal}  → a o≤ b → b o< osuc x → supf0 a ⊆' supf0 b 
-                mono {a} {b} a≤b b<ox = {!!}
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -623,7 +627,7 @@
      ... | no ¬ox with trio< x y
      ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
-     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} 
+     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!}
                      ; initial = {!!} ; 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
             field
@@ -662,19 +666,11 @@
          ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
          ... | case2 z<y  = ordtrans x<z z<y
-         u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
-         u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = um00 where -- ZChain.chain-mono (prev w ? ay) ? ? lt
-             um00 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev w a₁ ) w) i 
-             um00 = {!!}
-             um01 : odef  (ZChain.supf (prev z a ) z) i → odef  (ZChain.supf (prev z {!!} ) w) i 
-             um01 = {!!} -- ZChain.chain-mono (prev z a ay) {!!} {!!}
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = lt }
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( osuc-< w≤x c )
-         ... | tri≈ ¬a z=x ¬c | tri< w<x ¬b ¬c₁ = ⊥-elim ( osuc-< z≤w (subst (λ k → w o< k ) (sym z=x) w<x ) )
-         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = λ lt → lt 
-         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( osuc-< w≤x c ) -- o<> c ( ord≤< w≤x )) -- z≡w x o< w
-         ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< w≤x (ord≤< c  z≤w ) ) -- x o< z → x o< w 
+         u-mono : {z : Ordinal} → z o≤ x → supf0 z ⊆' supf0 x
+         u-mono {z} z≤x {i} with trio< z x 
+         ... | tri< a ¬b ¬c = {!!} -- λ lt → lt -- record { u = z ; u<x = a ; chain∋z = lt }
+         ... | tri≈ ¬a b ¬c = {!!} -- λ lt → lt 
+         ... | tri> ¬a ¬b c = {!!} -- λ lt → lt 
          
      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)
@@ -691,7 +687,7 @@
 
      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
+     SZ1 f mf {y} ay z = {!!} where -- 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
@@ -716,7 +712,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 zc1 ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 total ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
@@ -724,7 +720,8 @@
               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 )
+         total : IsTotalOrderSet (ZChain.chain zorn04)
+         total =  ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)) o≤-refl 
 
 -- usage (see filter.agda )
 --