# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654503485 -32400
# Node ID 95ec4d121e1269e05d811fad4de80a63b2ec29bb
# Parent  409215885fc0e34f1ff75a4d4bf570cf6a44b2c8
...

diff -r 409215885fc0 -r 95ec4d121e12 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 06 07:47:45 2022 +0900
+++ b/src/zorn.agda	Mon Jun 06 17:18:05 2022 +0900
@@ -249,33 +249,6 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
       fc∨sup :  {a : Ordinal } → a o< osuc z →  ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
-      -- mono : { a : Ordinal } → (ca : odef chain a) → (SA : HOD)  → IsSup A SA (chain⊆A ca) → SA  ⊆' chain
-
-ZCSet : (A : HOD)  (f : Ordinal → Ordinal ) → Ordinal → HOD
-
--- ZC is not strictly positive, because it occurs
--- in the first clause
-
-data ZC (A : HOD) (f : Ordinal → Ordinal ) : Ordinal → Set n where
-   zc-init : ZC A f o∅
-   zc-fc  : {s x : Ordinal} → (as : odef A s) → ZC A f s → HasPrev A (ZCSet A f s) as f → ZC A f x
-   zc-sup : {s x : Ordinal} → (as : odef A s) → ZC A f s → IsSup A   (ZCSet A f s) as → ZC A f x
-
-ZCSet A f s = record { od = record { def = λ x → ZC A f x } ; odmax = {!!} ; <odmax = {!!} }
-
-ZC→ZChain : (A : HOD) {x z : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
-    → ZC A f z → (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) → ZChain A ax f mf sup z
-ZC→ZChain A {x} {z} ax f mf zc sup = record {
-      chain = ZCSet A f x
-    ; chain⊆A = {!!} 
-    ; chain∋x = {!!} 
-    ; initial = {!!} 
-    ; f-total = {!!} 
-    ; f-next = {!!} 
-    ; f-immediate = {!!} 
-    ; is-max = {!!} 
-    ; fc∨sup = {!!}
-   }
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -570,7 +543,11 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = UnionZ where
+     ... | no ¬ox with trio< x y
+     ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b y<x = {!!} where
        UnionZ : ZChain A ay f mf supO x
        UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
@@ -591,23 +568,12 @@
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
-         u-chain∋x = {!!}
+         u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
          Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b )  → a o< b → b o< x → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub)
-         Uz-mono {a} {b} ua ub a<b b<x {i} uai = {!!} where
-             z30 : odef A b
-             z30 = (ZChain.chain⊆A (uzc ub) (UZFChain.chain∋z ub))
-             supa : SUP A (ZChain.chain (uzc ua))
-             supa = supP (ZChain.chain (uzc ua)) (ZChain.chain⊆A (uzc ua)) (ZChain.f-total (uzc ua)) 
-             in-chain :   HasPrev A (ZChain.chain (uzc ua)) (SUP.A∋maximal supa) f ∨ IsSup A (ZChain.chain (uzc ua)) (SUP.A∋maximal supa)
-             in-chain = {!!}
-             z31 : ZChain.chain (uzc ua) ∋ SUP.sup supa
-             z31 = ZChain.is-max (uzc ua) (ZChain.chain∋x (uzc ua)) {!!} (SUP.A∋maximal supa) {!!} {!!}
-             ai : odef A i
-             ai = ZChain.chain⊆A (uzc ua) uai
-             -- (ZChain.initial (uzc ua) uai)
-             z32 : IsSup A (ZChain.chain (uzc ub)) ai
-             z32 = record { x<sup = {!!} }
-
+         Uz-mono {a} {b} ua ub a<b b<x {i} = z40 where
+             z40 : odef (ZChain.chain (uzc ua)) i → odef (ZChain.chain (uzc ub)) i
+             z40 uai = ZChain.is-max (uzc ub) (ZChain.chain∋x (uzc ub)) {!!} {!!}
+                (ZChain.fc∨sup (uzc ub) {!!} {!!} ) ?
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux