# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651114930 -32400
# Node ID e1a33b1bc16cc720295ae89409a9b8c281424cc3
# Parent  f007e044b2c66cf31fabf60d3694412934c23e1f
...

diff -r f007e044b2c6 -r e1a33b1bc16c src/zorn.agda
--- a/src/zorn.agda	Thu Apr 28 11:47:18 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 12:02:10 2022 +0900
@@ -316,13 +316,13 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
-     3cases : {x y : Ordinal} → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )
-        → (ax : odef A x )→ (ay : odef A y )
-        → (zc0 :  ZChain A ay f mf supO x ) 
-        →  Prev< A (ZChain.chain zc0) ax f
-           ∨  (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x)
-           ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x ))
-     3cases {x} {y} f mf ax ay zc0 = {!!}
+     -- 3cases : {x y : Ordinal} → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )
+     --    → (ax : odef A x )→ (ay : odef A y )
+     --    → (zc0 :  ZChain A ay f mf supO x ) 
+     --    →  Prev< A (ZChain.chain zc0) ax f
+     --       ∨  (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x)
+     --       ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x ))
+     -- 3cases {x} {y} f mf ax ay zc0 = {!!}
      -- Union of ZFChain
      UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) 
             → ( (z : Ordinal) → z o< B → {y : Ordinal} →  (ya : odef A y) → ZChain A ya f mf supO z ) → HOD
@@ -395,7 +395,7 @@
                     zc6 : IsTotalOrderSet zc5
                     zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
                         ; compare = cmp }
-          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) ))
+          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
           ... | case1 x=sup = {!!} -- x is sup
           ... | case2 ¬x=sup = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!}
                      ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention