# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655459108 -32400
# Node ID d6ad1af5299ec5de204d2d2e67f8596b7d506863
# Parent  e0cd78095f1bfcaa3ae6e10ffefa081e477443a3
...

diff -r e0cd78095f1b -r d6ad1af5299e src/OD.agda
--- a/src/OD.agda	Fri Jun 17 16:21:28 2022 +0900
+++ b/src/OD.agda	Fri Jun 17 18:45:08 2022 +0900
@@ -215,6 +215,8 @@
 ≡od∅→=od∅  : {x : HOD} → x ≡ od∅ → od x == od od∅
 ≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x  ≡ k ) ord-od∅ ( cong & eq ) )
 
+-- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
+
 ∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
diff -r e0cd78095f1b -r d6ad1af5299e src/OrdUtil.agda
--- a/src/OrdUtil.agda	Fri Jun 17 16:21:28 2022 +0900
+++ b/src/OrdUtil.agda	Fri Jun 17 18:45:08 2022 +0900
@@ -74,6 +74,7 @@
 _o≤_ :  Ordinal → Ordinal → Set  n
 a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
+-- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
 
 xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
 xo<ab   {oa} {ob} a→b with trio< oa ob
diff -r e0cd78095f1b -r d6ad1af5299e src/zorn.agda
--- a/src/zorn.agda	Fri Jun 17 16:21:28 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 18:45:08 2022 +0900
@@ -258,7 +258,7 @@
    field
       supf : Ordinal → SupF A
       zc : ZChain A x f supf z
-      chain-mono : {x y : Ordinal} → x o< y → y o< osuc z →  * (SupF.chain (supf x )) ⊆' * (SupF.chain (supf y ))
+      chain-mono : {x y : Ordinal} → x o≤ y → y o< osuc z →  * (SupF.chain (supf x )) ⊆' * (SupF.chain (supf y ))
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -404,24 +404,6 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc1
           c = & (SUP.sup sp1)
 
-     -- ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
-     -- ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
-     -- init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain1 A y f  x
-     -- init-chain {y} {x} ay f mf x≤y = record { zc = record { chain⊆A = λ fx →  A∋fc y f mf {!!}
-     --                 ; f-total = {!!} ; f-next = λ {x} sx → {!!} 
-     --                 ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; chain-mono = {!!} } ; supf = supf } where
-     --           supf : Ordinal → SupF A
-     --           supf x = record { chain = & (ys ay f mf) }
-     --           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 →
-     --                b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
-     --                * a < * b → odef (ys ay f mf) b
-     --           is-max {a} {b} yca b≤x ab P a<b = {!!}
-     --           initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
-     --           initial {i} (init ai) = case1 refl
-     --           initial .{f x} (fsuc x lt) = {!!}
-
      --
      -- create all ZChains under o< x
      --
@@ -447,6 +429,8 @@
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
+          -- if previous chain satisfies maximality, we caan reuse it
+          --
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 A y f x
@@ -469,23 +453,39 @@
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                 ... | tri≈ ¬a b ¬c = sym *iso
                 ... | tri> ¬a ¬b c = sym *iso
-                mono : {a b  : Ordinal}  → a o< b → b o< osuc x →
+                seq<x : {b : Ordinal } → b o< x →  * (SupF.chain (supf b))  ≡ * (SupF.chain (supf0 b))
+                seq<x {b} b<x with trio< b x
+                ... | 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 →
                     * (SupF.chain (supf0 a )) ⊆' * (SupF.chain (supf0 b ))
-                mono {a} {b} a<b b<ox with osuc-≡< b<ox | trio< a x | trio< b x
-                ... | case1 b=x | tri< a₁ ¬b ¬c | tri< a₂ ¬b₁ ¬c₁ = ⊥-elim ( ¬b₁ b=x ) 
-                ... | case1 b=x | tri< a₁ ¬b ¬c | tri≈ ¬a b₁ ¬c₁ = subst (λ k →  _  ⊆' k ) {!!} ( ZChain1.chain-mono zc1 a<b {!!} )
-                ... | case1 b=x | tri< a₁ ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( ¬b₁ b=x )
-                ... | case1 b=x | tri≈ ¬a b₁ ¬c | u = {!!}
-                ... | case1 b=x | tri> ¬a ¬b c | u = {!!}
-                ... | case2 b<x | t | u = {!!}
-
+                mono {a} {b} a≤b b<ox with osuc-≡< a≤b
+                ... | case1 refl = λ x → x
+                ... | case2 a<b with osuc-≡< b<ox 
+                ... | case1 b=x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x) nc00 ( ZChain1.chain-mono zc1 a≤px <-osuc  ) where
+                     a<x : a o< x
+                     a<x with  osuc-≡< b<ox
+                     ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
+                     ... | case2 b<x = ordtrans a<b b<x
+                     a≤px : a o≤  px
+                     a≤px = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) a<x
+                     nc00 : * (SupF.chain (supf px))  ≡ * (SupF.chain (supf0 b))
+                     nc00 with trio< b x
+                     ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b=x )
+                     ... | tri≈ ¬a b ¬c = sym *iso
+                     ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b=x )
+                ... | case2 b<x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x ) (seq<x b<x )
+                            ( ZChain1.chain-mono zc1 a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) )
+                   where
+                     a<x : a o< x
+                     a<x with  osuc-≡< b<ox
+                     ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
+                     ... | case2 b<x = ordtrans a<b b<x
 
           zc4 : ZChain1 A y f x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax =  -- ¬ A ∋ p, just skip
-                 record { supf = supf ; zc = record { chain⊆A = {!!} ; initial = {!!}
-                     ; f-total = {!!} ; f-next =  {!!}  ; chain-mono = {!!} 
-                     ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}  } }  where -- no extention
+          ... | no noax = no-extenion zc11  where -- ¬ A ∋ p, just skip
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b
@@ -493,7 +493,7 @@
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt)  ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
-          ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | case1 pr = no-extenion zc17  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain0 = ZChain.chain zc0
                 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab →
@@ -501,13 +501,10 @@
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
-                zc9 :  ZChain1 A y f x
-                zc9 = record { zc = record { chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!} -- no extention
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} } }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
-                record { zc = record { chain = schain ; chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} } } where 
+                record { zc = record { chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!}
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  ; supf = supf0 ; chain-mono = mono } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -606,10 +603,26 @@
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
-          ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
-                   record { zc = record { chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }}  where
-                      -- no extention
+                supf0 : Ordinal → SupF A
+                supf0 z with trio< z x
+                ... | tri< a ¬b ¬c = supf z
+                ... | tri≈ ¬a b ¬c = record { chain = & schain }
+                ... | tri> ¬a ¬b c = record { chain = & schain }
+                seq : schain ≡ * (SupF.chain (supf0 x))
+                seq with trio< x x
+                ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
+                ... | tri≈ ¬a b ¬c = sym *iso
+                ... | tri> ¬a ¬b c = sym *iso
+                seq<x : {b : Ordinal } → b o< x →  * (SupF.chain (supf b))  ≡ * (SupF.chain (supf0 b))
+                seq<x {b} b<x with trio< b x
+                ... | 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 →
+                    * (SupF.chain (supf0 a )) ⊆' * (SupF.chain (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 zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0)   ab →
                             * a < * b → odef (ZChain.chain zc0) b
@@ -619,10 +632,9 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { zc = UnionZ ; supf = {!!} } where
-       UnionZ : ZChain A y f {!!} x
-       UnionZ = record { chain = Uz ; chain⊆A = {!!} ; f-total = {!!}  ; f-next = {!!} ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
+     ... | no ¬ox = record { supf = supf0 ; chain-mono = {!!}
+              ; zc  = record { chain⊆A = {!!} ; f-total = {!!}  ; f-next = {!!} 
+                     ; initial = {!!} ; f-immediate = {!!} ; 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
                u : Ordinal
@@ -643,6 +655,22 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) }
+         supf0 : Ordinal → SupF A
+         supf0 z with trio< z x
+         ... | tri< a ¬b ¬c = ZChain1.supf (prev z a {y} ay) z
+         ... | tri≈ ¬a b ¬c = record { chain = & Uz }
+         ... | tri> ¬a ¬b c = record { chain = & Uz }
+         seq : Uz ≡ * (SupF.chain (supf0 x))
+         seq with trio< x x
+         ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
+         ... | tri≈ ¬a b ¬c = sym *iso
+         ... | tri> ¬a ¬b c = sym *iso
+         seq<x : {b : Ordinal } → (b<x : b o< x ) →  * (SupF.chain (ZChain1.supf (prev b b<x {y} ay) b))  ≡ * (SupF.chain (supf0 b))
+         seq<x {b} b<x with trio< b x
+         ... | tri< a ¬b ¬c = ==→o≡ record { eq→ = ? ; eq← = ? }
+         --  cong (λ k → * (SupF.chain (ZChain1.supf (prev b k {y} ay) b)) ) {!!} --  b<x ≡ a
+         ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
+         ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)
          u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain (ZChain1.zc za)) i → odef (chain (ZChain1.zc zb)) i } uind i zai where
             open ZChain