# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667328173 -32400
# Node ID dfb4f7e9c45423fb5146b15e84471173662e77c9
# Parent  05f54e16f138411a2511edc5976cb38ff03aa098
...

diff -r 05f54e16f138 -r dfb4f7e9c454 src/zorn.agda
--- a/src/zorn.agda	Tue Nov 01 23:16:30 2022 +0900
+++ b/src/zorn.agda	Wed Nov 02 03:42:53 2022 +0900
@@ -80,7 +80,7 @@
 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
 ftrans<=-< : {x y z : Ordinal } →  x <=  y →  y << z →  x <<  z 
-ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) ? y<z
+ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) (sym (cong (*) eq))  y<z
 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z 
 
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 
@@ -582,12 +582,14 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
      --
-     -- Second TransFinite Pass for maximality
+     -- maximality of chain
+     --
+     --     supf is fixed for z ≡ & A , we can prove order and is-max
      --
 
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-     SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
+     SZ1 f mf {y} ay zc x = zc1 x where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) a≤b
@@ -634,8 +636,8 @@
           ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
           ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
 
-        zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
-        zc1 x prev with Oprev-p x  -- prev is not used now....
+        zc1 :  (x : Ordinal) → ZChain1 A f mf ay zc x
+        zc1 x with Oprev-p x  -- prev is not used now....
         ... | yes op = record { is-max = is-max ; order = order  } where
            px = Oprev.oprev op
            zc-b<x : {b : Ordinal } → ZChain.supf zc b o< ZChain.supf zc x → b o< osuc px
@@ -866,51 +868,61 @@
                  zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
                  zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where
                     u<x :  u o< x
-                    u<x = ?
+                    u<x =  supf-inject0 supf1-mono su<sx
+                    u≤px : u o≤ px
+                    u≤px = zc-b<x _ u<x
                     zc21 : {z1 : Ordinal } → FClosure A f (supf1 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< u px | inspect supf1 u
-                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u ? record {fcy<sup = zc13 ; order = zc17
-                         ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where
+                    zc21 (init asp refl ) with trio< (supf0 u) (supf0 px) | inspect supf1 u
+                    ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17
+                         ; supu=u = trans (sym (sf1=sf0 (o<→≤ u<px))) (ChainP.supu=u is-sup) } (init asp0 (sym (sf1=sf0 (o<→≤ u<px))) ) ⟫ where
+                        u<px :  u o< px
+                        u<px =  ZChain.supf-inject zc a
+                        asp0 : odef A (supf0 u)
+                        asp0 = ZChain.asupf zc 
                         zc17 :  {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u →
                             FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                        zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup 
-                         (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where
-                            zc19 : u o≤ px
-                            zc19 = o<→≤ a
+                        zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 u≤px)) ( ChainP.order is-sup 
+                         (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 u≤px)) ss<spx) (fcpu fc zc18) ) where
                             zc18 : s o≤ px
-                            zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19
+                            zc18 = ordtrans (ZChain.supf-inject zc ss<spx) u≤px
                         zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u )
-                        zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc )
-                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) )
-                    ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x  ⟫ )
+                        zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc )
+                    ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) 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  ⟫ )
                  zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z
                  zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫
                  zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where
-                        u<x :  u o< x
-                        u<x = ?
+                        u<px :  u o< px
+                        u<px = ZChain.supf-inject zc su<sx
+                        u<x : u o< x
+                        u<x = ordtrans u<px px<x
+                        u≤px : u o≤ px
+                        u≤px = o<→≤ u<px
+                        s1u<s1x : supf1 u o< supf1 x
+                        s1u<s1x = ordtrans<-≤ (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 u≤px )) (sym (sf1=sf0 o≤-refl)) su<sx) (supf1-mono (o<→≤ px<x) ) 
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 
                         zc21 (init asp refl ) with trio< u px | inspect supf1 u
                         ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u 
-                             ?  
-                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) } zc14 ⟫  where
+                             s1u<s1x 
+                                record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 u≤px ) (ChainP.supu=u is-sup) } zc14 ⟫  where
                             zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u →
                                   FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u)
-                            zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ ?))) ( ChainP.order is-sup 
-                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ ?)) ss<spx) (fcup fc s≤px) ) where
-                                  s≤px : s o≤ px
-                                  s≤px = ? -- ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x)
+                            zc17 {s} {z1} ss<su fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<px))) ( ChainP.order is-sup 
+                               (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<px)) ss<su) (fcup fc s≤px) ) where
+                                  s≤px : s o≤ px -- ss<su : supf1 s o< supf1 u
+                                  s≤px = ordtrans ( supf-inject0 supf1-mono ss<su ) (o<→≤ u<px)
                             zc14 : FClosure A f (supf1 u) (supf0 u)
-                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 ?)) asp) (sf1=sf0 ?)
+                            zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 u≤px)) asp) (sf1=sf0 u≤px)
                             zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u )
-                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) ( ChainP.fcy<sup is-sup fc )
-                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px ? record { fcy<sup = zc13 
+                            zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 u≤px )) ( ChainP.fcy<sup is-sup fc )
+                        ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (subst (λ k → supf1 k o< supf1 x) b s1u<s1x)  record { fcy<sup = zc13 
                               ; order = zc17 ; supu=u = zc18   } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b)))  ) ⟫ where
                             zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px )
                             zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc )
@@ -929,17 +941,19 @@
                                 zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b))
                                 s≤px : s o≤ px
                                 s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx)
-                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , ?  ⟫ )
+                        ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px  ⟫ )
                  zc12 {z} (case2 fc) = zc21 fc where
                         zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1
                         zc21 {z1} (fsuc z2 fc ) with zc21 fc
                         ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
                         ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ 
                         zc21 (init asp refl ) with  osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x )
-                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px ? -- (pxo<x op)
+                        ... | case1 sfpx=px =  ⟪ asp , ch-is-sup px zc18 
                                      record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where
                               zc15 : supf1 px ≡ px
                               zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px)
+                              zc18 : supf1 px o< supf1 x
+                              zc18 = ?
                               zc14 : FClosure A f (supf1 px) (supf0 px)
                               zc14 = init (subst (λ k → odef A k) (sym (sf1=sf0 o≤-refl)) asp) (sf1=sf0 o≤-refl)
                               zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px )
@@ -1309,37 +1323,6 @@
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x
      SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z  } (λ x → ind f mf ay x   ) x
 
-     data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
-            ( supf : Ordinal → Ordinal )  (z : Ordinal) : Set n where
-          zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z
-     
-     auzc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → {x : Ordinal } → ZChainP f mf ay supf x → odef A x
-     auzc f mf {y} ay supf {x} (zchain uz ucf) = proj1 ucf
-
-     zp-uz : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → {x : Ordinal } → ZChainP f mf ay supf x → Ordinal
-     zp-uz f mf ay supf (zchain uz _) = uz
-
-     uzc⊆zc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → {x : Ordinal } → (zp : ZChainP f mf ay supf x ) → UChain A f mf ay supf (zp-uz f mf ay supf zp) x 
-     uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-init fc ⟫) = ch-init fc 
-     uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-is-sup u u<x is-sup fc ⟫) with ChainP.supu=u is-sup
-     ... | eq = ch-is-sup u u<x is-sup fc 
-
-     UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → HOD
-     UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } 
-         ; odmax = & A ; <odmax = λ lt →  ∈∧P→o< ⟪ auzc f mf ay supf lt , lift true ⟫ }
-     
-     uzctotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-         → ( supf : Ordinal → Ordinal )
-         → IsTotalOrderSet (UnionZF f mf ay supf )
-     uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where 
-          uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub 
-             → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua )
-          uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb)
-
      msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → (zc : ZChain A f mf ay x ) 
          → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)