# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669448078 -32400
# Node ID 91988ae176abe6c6ae3b90e9a1c32e2ce4dba8db
# Parent  8b3d7c461a84c7bf0913f1d2e2ea417be4cd714c
...

diff -r 8b3d7c461a84 -r 91988ae176ab src/zorn.agda
--- a/src/zorn.agda	Sat Nov 26 07:51:09 2022 +0900
+++ b/src/zorn.agda	Sat Nov 26 16:34:38 2022 +0900
@@ -434,6 +434,7 @@
          {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f mf ay supf b) w
 
       asupf :  {x : Ordinal } → odef A (supf x)
+      supf-<= : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
 
@@ -524,6 +525,33 @@
    -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f mf ay supf (supf b)
    --    the condition of cfcs is satisfied, this is obvious
 
+record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+        {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
+   supf = ZChain.supf zc
+   field
+      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
+          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
+          → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
+
+record Maximal ( A : HOD )  : Set (Level.suc n) where
+   field
+      maximal : HOD
+      as : A ∋ maximal
+      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
+
+init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
+    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
+init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
+
+record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
+  field
+     i : Ordinal  
+     i<x : i o< x
+     fc : FClosure A f (supfz i<x) z 
+
+--
+-- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup
+--
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) 
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
@@ -596,66 +624,6 @@
                         z55 : FClosure A f (ZChain.supf zb u) z
                         z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 
-
-UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
-        {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
-        → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
-        → ( { x : Ordinal } → x o< z → supf x ≡ supf1 x)
-        → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x)
-        → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z
-UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x cp1 fc1 ⟫  where
-          fc1 : FClosure A f (supf1 u) x
-          fc1 = subst (λ k → FClosure A f k x ) (eq<x u<x) fc
-          supf1-mono : {x y : Ordinal } →  x o≤  y  → supf1 x o≤ supf1 y 
-          supf1-mono = ?
-          uc01 : {s : Ordinal } →  supf1 s o< supf1 u → s o< z
-          uc01 {s} s<u with trio< s z
-          ... | tri< a ¬b ¬c = a
-          ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> uc02  s<u ) where -- (supf-mono (o<→≤ u<x0))
-               uc02 :  supf1 u o≤ supf1 s
-               uc02 = begin
-                 supf1 u  ≤⟨ supf1-mono (o<→≤ u<x) ⟩
-                 supf1 z  ≡⟨ cong supf1 (sym b) ⟩
-                 supf1 s ∎  where open o≤-Reasoning O
-          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> uc03 s<u ) where
-               uc03 :  supf1 u o≤ supf1 s
-               uc03 = begin
-                 supf1 u  ≡⟨ sym (eq<x u<x) ⟩
-                 supf u  ≤⟨ supf-mono (o<→≤ u<x) ⟩
-                 supf z  ≤⟨ lex (o<→≤ c) ⟩
-                 supf1 s ∎  where open o≤-Reasoning O
-          cp1 : ChainP A f mf ay supf1 u
-          cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x) (ChainP.fcy<sup is-sup fc )  
-               ; order =  λ {s} {z} s<u fc  → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (eq<x u<x) 
-                  (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (eq<x (uc01 s<u) )) (sym (eq<x u<x)) s<u)  
-                    (subst (λ k → FClosure A f k z ) (sym (eq<x (uc01 s<u) )) fc ))
-               ; supu=u = trans (sym (eq<x u<x)) (ChainP.supu=u is-sup)  }
-
-record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
-        {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
-   supf = ZChain.supf zc
-   field
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z  → (ab : odef A b)
-          → HasPrev A (UnionCF A f mf ay supf z) f b ∨  IsSUP A (UnionCF A f mf ay supf b) ab
-          → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
-
-record Maximal ( A : HOD )  : Set (Level.suc n) where
-   field
-      maximal : HOD
-      as : A ∋ maximal
-      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
-
-init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
-    { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
-init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
-
-record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
-  field
-     i : Ordinal  
-     i<x : i o< x
-     fc : FClosure A f (supfz i<x) z 
-
 Zorn-lemma : { A : HOD }
     → o∅ o< & A
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
@@ -687,6 +655,9 @@
         ¬x<m :  ¬ (* x < * m)
         ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt)
 
+     --
+     -- we have minsup using LEM, this is similar to the proof of the axiom of choice
+     --
      minsupP :  ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → MinSUP A B
      minsupP B B⊆A total = m02 where
          xsup : (sup : Ordinal ) → Set n
@@ -987,8 +958,8 @@
 
           zc41 : ZChain A f mf ay x
           zc41 with zc43 x sp1
-          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono 
-              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
+          zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono 
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs  }  where
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px
@@ -1278,7 +1249,7 @@
                     ms01 {sup2} us P = MinSUP.minsup m us ?
 
 
-          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? 
+          zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ZChain.asupf zc ; supf-mono = ZChain.supf-mono zc 
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
                  --  supf0 px not is included by the chain
@@ -1381,6 +1352,23 @@
                       zc177 : supf0 z ≡ supf0 px
                       zc177 = ZChain.supfmax zc px<z  -- px o< z, px o< supf0 px
 
+                 zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) z → odef pchainpx z
+                 zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫
+                 zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc21 fc where
+                    u≤px : u o≤ px
+                    u≤px = zc-b<x _ u<x
+                    zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef pchainpx z1
+                    zc21 {z1} (fsuc z2 fc ) with zc21 fc
+                    ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
+                    ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫
+                    ... | case2 fc = case2 (fsuc _ fc)
+                    zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf0 u
+                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u u<px is-sup (init asp refl ) ⟫ where
+                        u<px :  u o< px
+                        u<px =  ZChain.supf-inject zc a
+                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym  b ))
+                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
                          tsup : MinSUP A (UnionCF A f mf ay supf0 z)
@@ -1419,6 +1407,8 @@
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+                     --  x o< sp      supf0 b ≡ supf0 x o≤ supf0 sp
+                     --      supf0 sp ≡ sp (?)
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) supf0 x
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x≤sup = λ {w} lt →
@@ -1430,7 +1420,8 @@
                      ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev
                                 ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } )
 
-     ... | no lim = ? where
+     ... | no lim = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono 
+              ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs    }  where
 
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
           pzc {z} z<x = prev z z<x
@@ -1446,7 +1437,7 @@
                zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
 
           aic : {z : Ordinal } → IChain A f supfz z → odef A z
-          aic {z} ic = ?
+          aic {z} ic =  A∋fc _ f mf (IChain.fc ic )
 
           zeq : {xa xb z : Ordinal } 
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 
@@ -1454,16 +1445,33 @@
           zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf ay xa≤xb  
               (pzc xa<x)  (pzc xb<x)  z≤xa
 
+          iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y 
+          iceq refl = cong supfz  o<-irr 
+
+          ifc≤ : {za zb : Ordinal } ( ia : IChain A f supfz za ) ( ib : IChain A f supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
+              → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za
+          ifc≤ {za} {zb} ia ib ia≤ib = subst (λ k → FClosure A f k _ ) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc) )   (IChain.fc ia)
+
           ptotalx : IsTotalOrderSet pchainx
           ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 with trio< (IChain.i ia) (IChain.i ib)
-               ... | tri< a ¬b ¬c = ?
-               ... | tri≈ ¬a b ¬c = ?
-               ... | tri> ¬a ¬b c = ?
+               uz01 with trio< (IChain.i ia)  (IChain.i ib)
+               ... | tri< ia<ib ¬b ¬c with 
+                    <=-trans (ZChain.supf-<= (pzc (ob<x lim (IChain.i<x ib))) ia<ib (ifc≤ ia ib (o<→≤ ia<ib))) (≤to<= (s≤fc _ f mf (IChain.fc ib)))
+               ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+                   ct00 : * (& a) ≡ * (& b)
+                   ct00 = cong (*) eq1
+               ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)  
+               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym (iceq ia=ib)) (IChain.fc ib)) 
+               uz01 | tri> ¬a ¬b ib<ia  with
+                    <=-trans (ZChain.supf-<= (pzc (ob<x lim (IChain.i<x ia))) ib<ia (ifc≤ ib ia (o<→≤ ib<ia))) (≤to<= (s≤fc _ f mf (IChain.fc ia)))
+               ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
+                   ct00 : * (& a) ≡ * (& b)
+                   ct00 = sym (cong (*) eq1)
+               ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1)    (λ eq → <-irr (case1 eq) lt) lt
 
           usup : MinSUP A pchainx
-          usup = minsupP pchainx (λ lt → ? ) ptotalx
+          usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc ic ) ) ptotalx
           spu = MinSUP.sup usup
 
           supf1 : Ordinal → Ordinal
@@ -1494,9 +1502,8 @@
           ... | tri≈ ¬a b ¬c = refl
           ... | tri> ¬a ¬b c = refl
 
-          -- zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z)
-          -- zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z) 
-          --        ? ? (init ? ?) ⟫           
+          zc11 : {z : Ordinal } → odef pchain z → odef pchainx z
+          zc11 {z} lt = ?
 
           sfpx<=spu : {z : Ordinal } → supf1 z <= spu
           sfpx<=spu {z} with trio< z x