# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655079734 -32400
# Node ID f48c9f4bafdbffef43e234ab2de8f607cfdd0eb9
# Parent  b3584dd8bafc9f46e1b71fd80a7fdf83bcd0b082
FCSet

diff -r b3584dd8bafc -r f48c9f4bafdb src/zorn.agda
--- a/src/zorn.agda	Sun Jun 12 12:20:16 2022 +0900
+++ b/src/zorn.agda	Mon Jun 13 09:22:14 2022 +0900
@@ -235,16 +235,28 @@
    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
+y1 : (A : HOD) → (y : Ordinal) → odef A y   → * (& (* y , * y)) ⊆' A
+y1 A y ay {x} lt with subst (λ k → odef k x) *iso lt
+... | case1 eq = subst (λ k → odef A k ) (sym (trans eq &iso)) ay
+... | case2 eq = subst (λ k → odef A k ) (sym (trans eq &iso)) ay
+
+record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p : Ordinal)   ( x : Ordinal ) : Set n where
    field
-      sup  : Ordinal
-      B∋sup  : odef B sup
-      issup  : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )  
-      minsup : {z : Ordinal} → (za : odef A z) → IsSup A B za → sup o≤ z
-      fc : FClosure A f sup x
+      ax : odef A x
+      fc∨sup :  FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → a << x )
+      -- f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → a << x1 ) → x o≤ x1
 
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
-                  ( z : Ordinal ) : Set (Level.suc n) where
+FCSet :  (A : HOD) → ( f : Ordinal → Ordinal ) → (sup : Ordinal) → HOD
+FCSet A f sup = record { od = record { def = λ x → FChain A f sup x } ; odmax = & A ; <odmax = fcs00 }
+   where
+     fcs00 :   {y : Ordinal} →  FChain A f sup y → y o< & A
+     fcs00  {y} fc = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (FChain.ax fc )))
+
+data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
+      Finit :  {z : Ordinal} → z ≡ (& (* y , * y))  → Fc∨sup A ay f z
+      Fc  :  {x : Ordinal} → (fc : Fc∨sup A ay f x ) →  Fc∨sup A ay f (& (FCSet A f x))
+
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
       chain⊆A : chain ⊆' A
@@ -256,8 +268,7 @@
       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 ) → IsMinSup A chain f ( chain⊆A ca)
-      sup≤z :  {a : Ordinal } → ( ca : odef chain a ) → IsMinSup.sup (fc∨sup ca)  o≤ z
+      fc∨sup :  {s c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A ca) f s ∧ odef (* s) c
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -585,46 +596,12 @@
             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 : {j : Ordinal} → FClosure A f (IsMinSup.sup (fc∨sup za zai)) j → odef (chain zb) j
-               um01 (fsuc x t) = f-next zb (um01 t)
-               um01 {j} (init as j=minsup ) with trio< j y
-               ... | tri< j<y ¬b ¬c = {!!}
-               ... | tri≈ ¬a j=y ¬c = {!!}
-               ... | tri> ¬a ¬b j>y = um10
-                where
-                 aj : odef A j
-                 aj = subst (λ k → odef A k ) (sym j=minsup) as
-                 zj : odef (chain za) j
-                 zj = subst (λ k → odef (chain za) k ) (sym j=minsup) ( IsMinSup.B∋sup (fc∨sup za zai) )
-                 j<a : j o< a
-                 j<a = {!!}
-                 um04 : j o< osuc b
-                 um04 = {!!}
-                 j<x : j o< x
-                 j<x = {!!}
-                 j<b : j o< b
-                 j<b = {!!}
-                 um05 : odef (chain (prev j j<x ay)) y
-                 um05 = {!!}
-                 um03 : * y < * j
-                 um03 with initial za zj
-                 ... | case1 eq = {!!}
-                 ... | case2 lt = lt
-                 um09 :  odef (chain (prev j j<x ay)) j
-                 um09 = {!!}
-                 um06 : IsSup A (chain (prev j j<x ay)) aj
-                 um06 = record { x<sup = λ {c} pc → um07 pc } where
-                    um08 : ZChain A y f j
-                    um08 = prev j j<x ay
-                    um07 : {c : Ordinal} → odef (chain (prev j j<x ay)) c →  (c ≡ j) ∨ (c << j)
-                    um07 {c} pc = {!!} where
-                       um11 : odef (chain za) c
-                       um11 = ?
-                       um10  : (c ≡ i) ∨ (c << i)
-                       um10  = IsMinSup.issup (fc∨sup za zai) um11
-                 um10 : odef (chain zb) j
-                 um10 = previ j j<a {!!} (prev j j<x ay ) zb um09 -- (is-max (prev j j<x ay ) um05 <-osuc aj (case2 um06) um03 )
+            uind a previ a<b za zb {i} zai = um01 where
+                FC : Fc∨sup A (chain⊆A za zai) f i ∧ odef {!!} i
+                FC = fc∨sup za zai 
+                um01 : odef (chain zb) i
+                um01 with FC
+                ... | t = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux