# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669629190 -32400
# Node ID 40532b0ed2302d9367690e75c983b1bb872806d0
# Parent  07ffcf16a3d4455969bab7a3ffdc80022d8f3136
...

diff -r 07ffcf16a3d4 -r 40532b0ed230 src/zorn.agda
--- a/src/zorn.agda	Mon Nov 28 07:13:19 2022 +0900
+++ b/src/zorn.agda	Mon Nov 28 18:53:10 2022 +0900
@@ -295,6 +295,7 @@
 ... | case2 lt =  tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct02 : * a < * b
           ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt
+fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri≈ a₁ ¬b ¬c = ?
 fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ?
 
 
@@ -310,9 +311,14 @@
 
 --      order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
 --
+
+data UChain  { A : HOD } { f : Ordinal → Ordinal }  
+       {supf : Ordinal → Ordinal} (x : Ordinal) : (z : Ordinal) → Set n where
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain x z
+
 UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f supf x
-   = record { od = record { def = λ z → odef A z ∧ ( { s : Ordinal} → s o< x → FClosure A f (supf s) z ) } ;   
+   = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} x z } ;   
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 
@@ -352,7 +358,7 @@
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
         → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
-chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup  ⟫ = ?
+chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
@@ -368,6 +374,7 @@
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
       supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
+      supf0 : supf o∅ ≡ y
 
       minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f supf x)
       supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
@@ -386,7 +393,7 @@
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ?   ⟫
    f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
-   f-next {a} ⟪ aa , ch-is-sup  ⟫ = ?
+   f-next {a} ⟪ aa , cp  ⟫ = ?
    initial : {z : Ordinal } → odef chain z → * y ≤ * z
    initial {a} ⟪ aa , ua ⟫  = ?
    f-total : IsTotalOrderSet chain
@@ -438,9 +445,9 @@
    supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
    supf-idem  mf< {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
-       z54 {w} ⟪ aw , fc ⟫ = order ? ? where
-               u<b : supf b o< b
-               u<b = ?
+       z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order su<b fc where
+               su<b : u o< b
+               su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫