# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654939992 -32400
# Node ID 4dbaa071d6959f1158864c3ff46164ca09fd5020
# Parent  f545b97ce7a823b254069fb3851a6b4b3de994f8
...

diff -r f545b97ce7a8 -r 4dbaa071d695 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 07 12:59:08 2022 +0900
+++ b/src/zorn.agda	Sat Jun 11 18:33:12 2022 +0900
@@ -93,15 +93,15 @@
 -- immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
 
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
-   init : odef A s → FClosure A f s s
+   init : {x : Ordinal} → odef A s → x ≡ s  → FClosure A f s x
    fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)
 
 A∋fc : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y
-A∋fc {A} s f mf (init as) = as
+A∋fc {A} s f mf (init as refl ) = as
 A∋fc {A} s f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} s  f mf fcy ) )
 
 s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y
-s≤fc {A} s {.s} f mf (init x) = case1 refl
+s≤fc {A} s {.s} f mf (init x refl ) = case1 refl
 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
 ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy )
 ... | case2 x<fx with s≤fc {A} s f mf fcy 
@@ -109,7 +109,7 @@
 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
 
 fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
-fcn s mf (init as) = zero
+fcn s mf (init as refl ) = zero
 fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p))
 ... | case1 eq = fcn s mf p
 ... | case2 y<fy = suc (fcn s mf p )
@@ -118,11 +118,11 @@
      → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
      fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
-     fc00 zero zero refl (init _) (init x₁) i=x i=y = refl
-     fc00 zero zero refl (init as) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as) cy i=x i=y )
-     fc00 zero zero refl (fsuc x cx) (init as) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as) i=x i=y )
+     fc00 zero zero refl (init _ refl ) (init x₁ refl ) i=x i=y = refl
+     fc00 zero zero refl (init as refl ) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as refl ) cy i=x i=y )
+     fc00 zero zero refl (fsuc x cx) (init as refl ) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
+     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as refl ) i=x i=y )
      fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
      ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
      fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
@@ -193,7 +193,7 @@
            cxx :  FClosure A f s (f x)
            cxx = fsuc x cx 
            fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
-           fc16 x (init as) with proj1 (mf s as )
+           fc16 x (init as refl ) with proj1 (mf s as )
            ... | case1 _ = case1 refl
            ... | case2 _ = case2 refl
            fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
@@ -235,6 +235,14 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
+record IsMinSup ( A B : HOD ) ( f : Ordinal → Ordinal ) {x : Ordinal} (xa : odef A x)  : Set n where
+   field
+      sup  : Ordinal
+      B∋sup  : odef B sup
+      issup  : {y : Ordinal} → odef B y → (x ≡ y ) ∨ (y << x )  
+      minsup : {z : Ordinal} → (za : odef A z) → IsSup A B za → sup o≤ z
+      fc : FClosure A f sup x
+
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
                   ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -248,32 +256,8 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      fc∨sup :  {a : Ordinal } → ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
-
-Uz-mono : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
-     → ( a b : Ordinal ) → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) 
-     → ZChain.chain za  ⊆' ZChain.chain zb
-Uz-mono A x f a b = TransFinite {λ a → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b)
-     → ZChain.chain za  ⊆' ZChain.chain zb } ind a where
-    open ZChain
-    ind :  (a : Ordinal)
-         → ((y : Ordinal) → y o< a →  y o< b → (za : ZChain A x f y) (zb : ZChain A x f b) → chain za ⊆' chain zb)
-         → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) → chain za ⊆' chain zb
-    ind a prev a<b za zb {i} zai with f-total za (subst (λ k → odef (chain za) k) (sym &iso) zai)
-                                     (subst (λ k → odef (chain za) k) (sym &iso) (chain∋x za) ) 
-    ... | tri< i<x ¬b ¬c with initial za zai
-    ... | case1 i=x = ⊥-elim ( ¬b (sym i=x))
-    ... | case2 x<i = ⊥-elim ( ¬c x<i)
-    ind a prev a<b za zb {i} zai | tri≈ ¬a b ¬c = subst (λ k → odef (chain zb) k ) (sym (*≡*→≡ b))(chain∋x zb)
-    ind a prev a<b za zb {i} zai | tri> ¬a ¬b x<i = um i zai where
-          um : (i : Ordinal ) → odef (chain za) i → odef (chain zb) i
-          um zai i with fc∨sup za zai
-          ... | case1 fc = {!!}
-          ... | case2 sup = {!!}
-          um01 : i o< osuc b
-          um01 = {!!}
-          um02 : {!!}
-          um02 =  is-max zb (chain∋x zb) {!!} (chain⊆A za zai)  {!!} x<i
+      fc∨sup :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup A chain f ( chain⊆A ca)
+      sup≤x :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup.sup (fc∨sup ca)  o≤ x
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -536,7 +520,7 @@
                     → HasPrev A schain ab f ∨ IsSup A schain ab   
                     → * a < * b → odef schain b
                 s-ismax {a} {b} sa b<ox ab p a<b with osuc-≡< b<ox -- b is x?
-                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) refl  ))
                 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where   -- has previous
                      z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
@@ -594,6 +578,31 @@
          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 = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
+         u-mono :  ( a b : Ordinal ) → b o< x → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
+         u-mono a b b<x = TransFinite {λ a → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b)
+             → ZChain.chain za  ⊆' ZChain.chain zb } uind a where
+            open ZChain
+            uind :  (a : Ordinal)
+                 → ((c : Ordinal) → c o< a →  c o< b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
+                 → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
+            uind a previ a<b za zb {i} zai = um01 (IsMinSup.fc (fc∨sup za zai)) where
+               um01 : {i : Ordinal} → FClosure A f (IsMinSup.sup (fc∨sup za zai)) i → odef (chain zb) i
+               um01 (fsuc x t) = f-next zb (um01 t)
+               um01 {j} (init s j=minsup ) with trio< j b
+               ... | tri> ¬a ¬b b<j = {!!}
+               ... | tri≈ ¬a b=j ¬c = {!!}
+               ... | tri< j<b ¬b ¬c = previ j j<a j<b {!!} zb {!!}
+                where
+                 zj : ZChain A y f j
+                 zj = prev (osuc j) j<x ay
+                 um10 : j ≡ IsMinSup.sup (fc∨sup za zai)
+                 um10 = j=minsup
+                 -- zcj : odef (chain zj  ) j
+                 -- zcj = ZChain.is-max zj {!!} {!!} {!!} (case2 ?) {!!}
+                 j<a  : j o< a
+                 j<a  = {!!}
+                 -- um00 : odef (chain zb) j
+                 -- um00 = previ (osuc j) {!!} {!!} zj zb zcj 
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux