# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659029917 -32400
# Node ID 9e34893d9a030c631639669513b06432a85c00cc
# Parent  6aafa22c951a939c6c078e3f590f0fdeba3e8150
...

diff -r 6aafa22c951a -r 9e34893d9a03 src/zorn.agda
--- a/src/zorn.agda	Thu Jul 28 10:01:43 2022 +0900
+++ b/src/zorn.agda	Fri Jul 29 02:38:37 2022 +0900
@@ -73,10 +73,20 @@
 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 ≤-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 refl ) (case1 refl ) = case1 refl
+<-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
+<-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
+<-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
+
 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 
 <=to≤ (case1 eq) = case1 (cong (*) eq)
 <=to≤ (case2 lt) = case2 lt
 
+≤to<= : {x y : Ordinal } → * x ≤ * y → x <= y 
+≤to<= (case1 eq) = case1 ( subst₂ (λ j k → j ≡ k ) &iso &iso  (cong (&) eq) )
+≤to<= (case2 lt) = case2 lt
+
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
@@ -248,13 +258,15 @@
 
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
    field
-      x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
+      x<sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+      min-sup : {z : HOD } → B ∋ z → ( {x : HOD } → B ∋ x → (x ≡ z ) ∨ (x < z ) ) 
+          → (z ≡ sup ) ∨ (sup < z )  
 
 --
 --  sup and its fclosure is in a chain HOD
@@ -668,6 +680,25 @@
      -- create all ZChains under o< x
      --
 
+     record FChain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (x : Ordinal) : Set n where
+        field
+            supf     : Ordinal → Ordinal
+            fcy<sup : { z : Ordinal ) → FClosure A f y z → z <= supf x
+            is-sup : ( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= supf x
+            is-minsup : ( x1 : Ordinal ) → 
+                (( z : Ordinal ) → (z<x : z o< x ) → { z1 : Ordinal } → FClosure A f (supf z) z1 → z1 <= x1 ) → supf x <= x1
+        order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
+        order = ?
+
+
+     fsupf : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal ) → FChain A f mf ay x
+     fsupf f mf {y} ay x = TransFinite0 find x where
+          find : (x : Ordinal ) →  (( z : Ordinal ) → z o< x → FChain A f mf ay z ) → FChain A f mf ay x 
+          find x prev with trio< o∅ x
+          ... | tri< a ¬b ¬c = ?
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
+
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
      ind f mf {y} ay x prev with Oprev-p x
@@ -753,55 +784,10 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay psupf0 ( (proj2 ca)) ( (proj2 cb)) 
 
-
           usup : SUP A pchain0
           usup = supP pchain0 (λ lt → proj1 lt) ptotal0
           spu = & (SUP.sup usup)
 
-          record Usupf ( w : Ordinal ) : Set n where
-             field
-                supf : Ordinal → Ordinal
-                uniq-supf : {z w1 : Ordinal } → z o< w1 → (w<x : w o< x) → (w1<w : w1 o< w) 
-                    →  supf z ≡ ZChain.supf (prev w1 (ordtrans w1<w w<x )) z
-         
-          US : (w1 : Ordinal) → w1 o< x → Usupf w1
-          US w1 w1<x = TransFinite0 uind w1 where
-              uind :  (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w
-              uind w uprev with Oprev-p x
-              ... | yes op = record { supf = ? ; uniq-supf = ? } where
-                  px = Oprev.oprev op
-                  zc : ZChain A f mf ay (Oprev.oprev op)
-                  zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
-                  supf : Ordinal → Ordinal 
-                  supf z with trio< z w
-                  ... | tri< a ¬b ¬c = ZChain.supf (prev _ ?) z
-                  ... | tri≈ ¬a b ¬c = ZChain.supf zc z
-                  ... | tri> ¬a ¬b c = ZChain.supf zc z
-                  us : {z : Ordinal } → z o< w → (w<x : w o< x) → supf z ≡ ZChain.supf (prev _ w<x) z
-                  us {z} z<w w<x with trio< z w
-                  ... | tri< a ¬b ¬c = u01 where
-                      u02 :  ? ≡ Usupf.supf (uprev z a) z
-                      u02 = ?
-                      u01 : ZChain.supf (prev ? ?) z ≡ ZChain.supf (prev w w<x) z
-                      u01 = ? -- subst (λ k → k ≡ _ ) ? ( Usupf.uniq-supf (uprev _ ?) ? ? )
-                  ... | tri≈ ¬a b ¬c = ?
-                  ... | tri> ¬a ¬b c = ?
-              ... | no wlim = record { supf = supf ; uniq-supf = ? } where
-                  supf : Ordinal → Ordinal 
-                  supf z with trio< (osuc z) w
-                  ... | tri< a ¬b ¬c = Usupf.supf ( uprev (osuc z) a ) z
-                  ... | tri≈ ¬a b ¬c = spu
-                  ... | tri> ¬a ¬b c = spu
-                  us : {z : Ordinal} {w2 : Ordinal} → z o< w2 
-                     → (w<x : w o< x) (w2<w : w2 o< w) → supf z ≡ ZChain.supf (prev w2 (ordtrans w2<w w<x)) z
-                  us {z} {w2} z<w2 w<x w2<w with trio< (osuc z) w
-                  ... | tri< a ¬b ¬c = ? where
-                      u00 =  Usupf.uniq-supf (uprev (osuc z) ?)  ? ? ? 
-                      u01 =  Usupf.uniq-supf (uprev w2 ?)  ? ? ?
-                  ... | tri≈ ¬a b ¬c = ?
-                  ... | tri> ¬a ¬b c = ?
-
-
           psupf : Ordinal → Ordinal
           psupf z with trio< z x 
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
@@ -822,6 +808,11 @@
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
               ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
 
+          order :  {b sup1 z1 : Ordinal} → b o< x →
+            psupf sup1 o< psupf b →
+            FClosure A f (psupf sup1) z1 → (z1 ≡ psupf b) ∨ (z1 << psupf b)
+          order {b} {s} {z1}  b<x ps<pb fc = ?
+
           csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
           csupf z with trio< z x | inspect psupf z
           ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
@@ -836,26 +827,8 @@
                       zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
                       ... | case1 eq = case1 (trans eq (sym eq1) )
                       ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
-                      zc21 :  {sup1 z1 : Ordinal} → psupf sup1 o< psupf z → FClosure A f (psupf sup1) z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
-                      zc21 {s} {z1} s<z fc = zc22 where
-                        zc25 : psupf z ≡ ZChain.supf ozc z 
-                        zc25 = psupf<z z<x
-                        s<x : s o< x
-                        s<x = {!!}
-                        zc26 : psupf s ≡ ZChain.supf (pzc (osuc s) (ob<x lim s<x))  s 
-                        zc26 = psupf<z s<x
-                        zc23 : ZChain.supf ozc s o< ZChain.supf ozc z
-                        zc23 = {!!}
-                        zc24 : FClosure A f (ZChain.supf ozc s) z1
-                        zc24 with trio< s x
-                        ... | t = {!!}
-                        zc22 : (z1 ≡ psupf z) ∨ (z1 << psupf z)
-                        zc22 with ZChain.order ozc <-osuc zc23 zc24 
-                        ... | case1 eq = case1 (trans eq (sym eq1) )
-                        ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
-                      cp1 = record {  fcy<sup = zc20   ; order = zc21 }
-
+                      cp1 = record {  fcy<sup = zc20   ; order = order z<x  }
                      ---  u = supf u = supf z 
           ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup {!!} {!!} {!!} ⟫ where
                 sa = SUP.A∋maximal usup