# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663635983 -32400
# Node ID eaa863c4ebe8084c0ff88be7ebbb4dd4f409a896
# Parent  23dcb59d1231fe6ef30f6756920aa240216d1255
...

diff -r 23dcb59d1231 -r eaa863c4ebe8 src/zorn.agda
--- a/src/zorn.agda	Sat Sep 17 15:11:13 2022 +0900
+++ b/src/zorn.agda	Tue Sep 20 10:06:23 2022 +0900
@@ -375,6 +375,7 @@
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supf-max : {x : Ordinal } → supf x o≤ supf z
       supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
+      x≤supfx : {x : Ordinal } → x o≤ supf x
       csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -408,16 +409,7 @@
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
    supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
-   supf-idem = ?
-
-   x≤supfx : {x : Ordinal } → x o≤ supf x
-   x≤supfx {x} with trio< x (supf x)
-   ... | tri< a ¬b ¬c = o<→≤ a
-   ... | tri≈ ¬a b ¬c = o≤-refl0 b
-   ... | tri> ¬a ¬b c = ? --   supf x o< x
-   -- with osuc-≡< (supf-mono (o<→≤ c) )
-   -- ... | case1 eq = ?
-   -- ... | case2 lt = ⊥-elim ( o<¬≡ supf-idem lt)
+   supf-idem {x} = ?
 
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
@@ -428,21 +420,6 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
-   csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
-   csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z record { fcy<sup = fcy<sup (o<→≤ sb<z) ; order = order ; supu=u = supf-idem }  (init (subst (λ k → odef A k) (sym supf-idem) asb)  supf-idem ) ⟫ where
-        b<z : b o< z
-        b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z x≤supfx  )
-        asb : odef A (supf b)
-        asb = supf∈A (o<→≤ b<z)
-        supb : SUP A (UnionCF A f mf ay supf (supf b))
-        supb = sup (o<→≤ sb<z)
-        supb-is-b : supf (supf b) ≡ & (SUP.sup supb)
-        supb-is-b = supf-is-sup (o<→≤ sb<z)
-        order : {s z1 : Ordinal} → supf s o< supf (supf b) →
-            FClosure A f (supf s) z1 → (z1 ≡ supf (supf b)) ∨ (z1 << supf (supf b))
-        order {s} {z1} ss<ssb fs with SUP.x<sup supb ?
-        ... | case1 eq = ?
-        ... | case2 lt = ?
 
    -- ordering is not proved here but in ZChain1 
 
@@ -528,11 +505,22 @@
      chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
             ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x a≤b ) is-sup fc  ⟫ 
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& 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)
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         (zc : ZChain A f mf ay x ) → SUP A (ZChain.chain zc)
+     sp0 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
+        ztotal : IsTotalOrderSet (ZChain.chain zc) 
+        ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
+
+     x≤sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         (zc : ZChain A f mf ay x ) → x o≤ & (SUP.sup (sp0 f mf ay zc))
+     x≤sp0 f mf {x} ay zc with trio< x (& (SUP.sup (sp0 f mf ay zc))) 
+     ... | tri< a ¬b ¬c = o<→≤ a
+     ... | tri≈ ¬a b ¬c = o≤-refl0 b
+     ... | tri> ¬a ¬b sp<sp0 = ? where
+           sp1 :  {z : Ordinal } → z o≤ x  → SUP A (UnionCF A f mf ay (ZChain.supf zc) z)
+           sp1 {z} z≤x = ZChain.sup zc z≤x
 
      --
      -- Second TransFinite Pass for maximality
@@ -653,11 +641,10 @@
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
-            → (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
+            → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
+     fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc total
+           sp1 = sp0 f mf as0 zc 
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
@@ -680,8 +667,13 @@
                    ... | 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 total ))) ≡ & (SUP.sup (sp0 f mf zc total ))
-           z14 with total (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           ztotal : IsTotalOrderSet (ZChain.chain zc)
+           ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf as0 (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
+
+           z14 :  f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
+           z14 with ztotal (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.as sp1 ))
@@ -701,15 +693,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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& 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.as  sp1 ))))
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
+     z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
           sp1 : SUP A (ZChain.chain zc)
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
           c = & (SUP.sup sp1)
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
@@ -902,8 +892,26 @@
                  ... | tri≈ ¬a b ¬c = record { tsup = ?  ; tsup=sup = ? }
                  ... | tri> ¬a ¬b px<z = record { tsup = ? ; tsup=sup = ? }
 
+                 -- csupf1 : {b : Ordinal } → supf1 b o< z → odef (UnionCF A f mf ay supf1 z) (supf1 b) 
+                 -- csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z 
+                 --     record { fcy<sup = ZChain.fcy<sup zc (o<→≤ sb<z) ; order = order ; supu=u = ZChain.supf-idem zc }  
+                 --        (init (subst (λ k → odef A k) (sym (ZChain.supf-idem zc) asb))  (ZChain.supf-idem zc)) ⟫ where
+                 --    b<z : b o< z
+                 --    b<z = supf-inject0 (ZChain.supf-mono zc ( ordtrans<-≤ sb<z x≤supfx  ))
+                 --    asb : odef A (supf b)
+                 --    asb = supf∈A (o<→≤ b<z)
+                 --    supb : SUP A (UnionCF A f mf ay supf (supf b))
+                 --    supb = ZChain.sup zc (o<→≤ sb<z)
+                 --    supb-is-b : supf (supf b) ≡ & (SUP.sup supb)
+                 --    supb-is-b = ZChain.supf-is-sup zc (o<→≤ sb<z)
+                 --    order : {s z1 : Ordinal} → supf s o< supf (supf b) →
+                 --        FClosure A f (supf s) z1 → (z1 ≡ supf (supf b)) ∨ (z1 << supf (supf b))
+                 --    order {s} {z1} ss<ssb fs with SUP.x<sup supb ?
+                 --    ... | case1 eq = ?
+                 --    ... | case2 lt = ?
+
           ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
-              ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
+                          ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
@@ -1175,7 +1183,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 total ) where
+     ... | 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
@@ -1183,10 +1191,6 @@
               zc5 = ⟪  Maximal.as 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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
-         total : IsTotalOrderSet (ZChain.chain zorn04)
-         total {a} {b} = zorn06  where
-             zorn06 :  odef (ZChain.chain zorn04) (& a) → odef (ZChain.chain zorn04) (& b) → Tri (a < b) (a ≡ b) (b < a)
-             zorn06 = ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
 
 -- usage (see filter.agda )
 --