# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668900984 -32400
# Node ID 88fae58f89f521bd6c3c7cf6cf9ad52804d71e90
# Parent  ac182ad5bfd2185a55a0dc933285c5921e492d29
...

diff -r ac182ad5bfd2 -r 88fae58f89f5 src/OD.agda
--- a/src/OD.agda	Sat Nov 19 00:04:35 2022 +0900
+++ b/src/OD.agda	Sun Nov 20 08:36:24 2022 +0900
@@ -100,7 +100,7 @@
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
-  sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
+  sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ 
 -- possible order restriction
   ho< : {x : HOD} → & x o< next (odmax x)
 
@@ -302,10 +302,10 @@
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 
 Replace : HOD  → (HOD  → HOD) → HOD 
-Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
+Replace X ψ = record { od = record { def = λ x → (x o≤ sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
     ; odmax = rmax ; <odmax = rmax<} where 
         rmax : Ordinal
-        rmax = sup-o X (λ y X∋y → & (ψ (* y)))
+        rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y))))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 
@@ -342,7 +342,7 @@
 A ∈ B = B ∋ A
 
 OPwr :  (A :  HOD ) → HOD 
-OPwr  A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) )   
+OPwr  A = Ord ( osuc ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) ) )
 
 Power : HOD  → HOD 
 Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x )
@@ -433,10 +433,11 @@
 selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y 
 selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
 
-sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y))))
-sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt )
+sup-c≤ :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o≤ (sup-o X (λ y X∋y → & (ψ (* y))))
+sup-c≤ ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o≤ X lt )
+
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where 
+replacement← {ψ} X x lt = ⟪ sup-c≤ ψ {X} {x} lt , lemma ⟫ where 
     lemma : def (in-codomain X ψ) (& (ψ x))
     lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
@@ -477,8 +478,8 @@
     lemma1  {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq ))
     lemma2 : (& t) o< (osuc (& (Ord a)))
     lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t))) 
-    lemma :  & ((Ord a) ∩ (* (& t)) ) o< sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x)))
-    lemma = sup-o< _ lemma2
+    lemma :  & ((Ord a) ∩ (* (& t)) ) o≤ sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x)))
+    lemma = sup-o≤ _ lemma2
 
 -- 
 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (& A)) first
@@ -519,8 +520,8 @@
     sup1 =  sup-o (Ord (osuc (& (Ord (& A))))) (λ x A∋x → & ((Ord (& A)) ∩ (* x)))
     lemma9 : def (od (Ord (Ordinals.osuc O (& (Ord (& A)))))) (& (Ord (& A)))
     lemma9 = <-osuc 
-    lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o< sup1
-    lemmab = sup-o< (Ord (osuc (& (Ord (& A))))) lemma9 
+    lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o≤ sup1
+    lemmab = sup-o≤ (Ord (osuc (& (Ord (& A))))) lemma9 
     lemmad : Ord (osuc (& A)) ∋ t
     lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) &iso (t→A (d→∋ t lt))) 
     lemmac : ((Ord (& A)) ∩  (* (& (Ord (& A) )))) =h= Ord (& A)
@@ -533,13 +534,13 @@
     lemmae = cong (λ k → & k ) ( ==→o≡ lemmac)
     lemma7 : def (od (OPwr (Ord (& A)))) (& t)
     lemma7 with osuc-≡< lemmad
-    lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
+    lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o≤ sup1) lemmae lemmab )
     lemma7 | case1 eq with osuc-≡< (⊆→o≤ {* (& t)} {* (& (Ord (& t)))} (λ {x} lt → lemmah lt )) where
         lemmah : {x : Ordinal } → def (od (* (& t))) x → def (od (* (& (Ord (& t))))) x
         lemmah {x} lt = subst (λ k → def (od k) x ) (sym *iso) (subst (λ k → k o< (& t))
             &iso
             (c<→o< (subst₂ (λ j k → def (od j)  k) *iso (sym &iso) lt )))
-    lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where 
+    lemma7 | case1 eq | case1 eq1 = subst (λ k → k o≤ sup1) (trans lemmae lemmai) lemmab where 
         lemmai : & (Ord (& A)) ≡ & t
         lemmai = let open ≡-Reasoning in begin
                 & (Ord (& A)) 
@@ -552,7 +553,7 @@
             ≡⟨ &iso ⟩
                 & t 
             ∎
-    lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
+    lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o≤ sup1) lemmae lemmab ) where
         lemmak : & (* (& (Ord (& t)))) ≡ & (Ord (& A))
         lemmak = let open ≡-Reasoning in begin
                 & (* (& (Ord (& t))))
@@ -563,9 +564,9 @@
             ∎
         lemmaj : & t o< & (Ord (& A))
         lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt 
-    lemma1 : & t o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))
-    lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
-        lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 )
+    lemma1 : & t o≤ sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))
+    lemma1 = subst (λ k → & k o≤ sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
+        lemma4 (sup-o≤ (OPwr (Ord (& A))) lemma7 )
     lemma2 :  def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t)
     lemma2 not = ⊥-elim ( not (& t) ⟪ lemma3 , lemma6 ⟫ ) where
         lemma6 : & t ≡ & (A ∩ * (& t)) 
diff -r ac182ad5bfd2 -r 88fae58f89f5 src/zorn.agda
--- a/src/zorn.agda	Sat Nov 19 00:04:35 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 08:36:24 2022 +0900
@@ -525,6 +525,34 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
+spuf-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
+spuf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
+       supfa = ZChain.supf za
+       supfb = ZChain.supf zb
+       ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
+       ind x prev x≤xa = ? where
+           sax=m : supfa x ≡ MinSUP.sup (ZChain.minsup za x≤xa )
+           sax=m = ZChain.supf-is-minsup za x≤xa 
+           sbx=m : supfb x ≡ MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))
+           sbx=m = ZChain.supf-is-minsup zb (OrdTrans x≤xa xa≤xb )
+           sxa=sxb : supfa x ≡ supfb x
+           sxa=sxb with trio< (supfa x) (supfb x)
+           ... | tri≈ ¬a b ¬c = b
+           ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (
+               begin
+                 supfb x  ≡⟨ ? ⟩
+                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≤⟨ MinSUP.minsup ? ? ? ⟩
+                 MinSUP.sup (ZChain.minsup za x≤xa ) ≡⟨ ? ⟩ 
+                 supfa x ∎ ) a ) where open o≤-Reasoning O
+           ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
+               begin
+                 supfa x  ≡⟨ ? ⟩
+                 MinSUP.sup (ZChain.minsup za x≤xa )  ≤⟨ MinSUP.minsup ? ? ? ⟩
+                 MinSUP.sup (ZChain.minsup zb (OrdTrans x≤xa xa≤xb ))  ≡⟨ ? ⟩
+                 supfb x ∎ ) c ) where open o≤-Reasoning O
+
 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 )
@@ -831,6 +859,12 @@
            ax : odef A x
            is-sup : IsMinSUP A B f ax
 
+     zc43 : (x sp1 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
+     zc43 x sp1 with trio< x sp1
+     ... | tri< a ¬b ¬c = case1 a
+     ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
+     ... | tri> ¬a ¬b c = case2 (o<→≤ c)
+
      --
      -- create all ZChains under o< x
      --
@@ -931,14 +965,8 @@
           --     supf0 px o≤ sp1
           --
 
-          zc43 : (x : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
-          zc43 x with trio< x sp1
-          ... | tri< a ¬b ¬c = case1 a
-          ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
-          ... | tri> ¬a ¬b c = case2 (o<→≤ c)
-
           zc41 : ZChain A f mf ay x
-          zc41 with zc43 x
+          zc41 with zc43 x sp1
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = ?  }  where
 
@@ -1007,11 +1035,8 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 --  supf0 a ≡ px we cannot use previous cfcs
+                 --  supf0 a ≡ px we cannot use previous cfcs, it is in the chain because
                  --       supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x
-                 --    supf0 a o< sp1 ≡ x
-                 --    sp1 ≡ px ≡ supf0 a o< x
-                 --    sp1 o< px ≡ supf0 a → ⊥
                  -- 
                  cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
                      → a o< b → b o≤ x → supf1 a o< x  → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
@@ -1255,79 +1280,34 @@
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z  
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
           pchain1 : HOD
           pchain1 = UnionCF A f mf ay supf1 x
 
-          is-max-hp : (supf : Ordinal → Ordinal) (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-                b o< x → (ab : odef A b) →
-                HasPrev A (UnionCF A f mf ay supf x) f b  →
-                * a < * b → odef (UnionCF A f mf ay supf x) b
-          is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
-          ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫
-          ... | ⟪ ab0 , ch-is-sup u u<x is-sup fc ⟫ = ? -- ⟪ ab ,
-                     -- subst (λ k → UChain A f mf ay supf x k )
-                     --     (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x is-sup (fsuc _ fc))  ⟫
-
-          zc70 : HasPrev A pchain f x  → ¬ xSUP pchain f x
-          zc70 pr xsup = ?
+          sfpx<=spu : {z : Ordinal } → supf1 z <= spu
+          sfpx<=spu {z} = ? -- MinSUP.x≤sup usup (case2 (init (ZChain.asupf zc {px}) refl ))
 
-          no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) supf0 x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = ? where -- record { supf = supf1  ; sup=u = sup=u
-               -- ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
-                 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
-                 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
-                 pchain0=1 : pchain ≡ pchain1
-                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
-                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
-                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                     zc10 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc12 fc where
-                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
-                          zc12 (fsuc x fc) with zc12 fc
-                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                          ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
-                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u ? ? (init ? ? ) ⟫
-                     zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
-                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                     zc11 {z} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = zc13 fc where
-                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
-                          zc13 (fsuc x fc) with zc13 fc
-                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫
-                          ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u<x is-sup (fsuc _ fc₁) ⟫
-                          zc13 (init asu su=z ) with trio< u x
-                          ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u ? ? (init ? ? ) ⟫
-                          ... | tri≈ ¬a b ¬c = ?
-                          ... | tri> ¬a ¬b c = ? -- ⊥-elim ( o≤> u<x c )
-                 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
-                 sup {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
-                 sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))
-                 sis {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = {!!} where
-                     zc8 = ZChain.supf-is-minsup (pzc z a) {!!}
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsMinSUP A (UnionCF A f mf ay supf1 b) f ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf1 b) f b ) → supf1 b ≡ b
-                 sup=u {z} ab z≤x is-sup with trio< z x
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x≤sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x≤sup = {!!} }
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x ))
+          sfpx≤spu : {z : Ordinal } → supf1 z o≤ spu
+          sfpx≤spu {z} = ? -- subst ( λ k → k o≤ spu) (sym (ZChain.supf-is-minsup zc o≤-refl ))  
+            -- ( MinSUP.minsup (ZChain.minsup zc o≤-refl) (MinSUP.asm supu)  
+            --  (λ {x} ux → MinSUP.x≤sup supu (case1 ux)) )
+
+          supf-mono : {x y : Ordinal } → x o≤  y → supf1 x o≤ supf1 y
+          supf-mono {x} {y} x≤y = ?
 
           zc5 : ZChain A f mf ay x
-          zc5 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain f x  )
-               -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension {!!}
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsMinSUP A pchain f ax )
-          ... | case1 is-sup = ? -- record { supf = supf1  ; sup=u = {!!}
-               -- ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?)
-          ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
+          zc5 with zc43 x spu
+          zc5 | (case2 sp≤x ) =  ? where
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                     → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
+          zc5 | (case1 x<sp ) =  ? where
+                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                     → a o< b → b o≤ x →  supf1 a o< x → FClosure A f (supf1 a) w → odef (UnionCF A f mf ay supf1 b) w
+                 cfcs mf< {a} {b} {w} a<b b≤x sa<x fc = ?
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function