# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656321429 -32400
# Node ID 18357e4bddba200c4f387f4d064d57aa6a536e4e
# Parent  3f0963e1c79f76b629812661701cf38196e61696
ZChain1 is not strictly positive

diff -r 3f0963e1c79f -r 18357e4bddba src/zorn.agda
--- a/src/zorn.agda	Mon Jun 27 16:26:39 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 18:17:09 2022 +0900
@@ -418,7 +418,7 @@
                      ; f-next =  ZChain.f-next zc  ; chain  = ZChain.chain zc 
                      ; chain∋x  = ZChain.chain∋x  zc
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
-                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) ? is-max } 
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) {!!} is-max } 
 
           zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
@@ -578,16 +578,16 @@
              no-extrention1 : ( {a b : Ordinal} → odef (chain zc0) a → b o< osuc x → (ab : odef A b) →
                      HasPrev A (chain zc0) ab f ∨  IsSup A (chain zc0) ab →
                              * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 y f x
-             no-extrention1 imx = record { zc = sz00  ; chain-mono = ? ; f-total = ?  } where
+             no-extrention1 imx = record { zc = sz00  ; chain-mono = {!!} ; f-total = {!!}  } where
                   sz00 : {z : Ordinal} → z o≤ x → ZChain A y f z 
-                  sz00 {z} z≤x = ?
+                  sz00 {z} z≤x = {!!}
              sz02 : ZChain1 y f x
              sz02 with ODC.∋-p O A (* x)
-             ... | no noax = no-extrention1 ?
+             ... | no noax = no-extrention1 {!!}
              ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain zc0) ax f ) 
-             ... | case1 pr = record { zc = ? ;  chain-mono = ? ; f-total = ? } where
+             ... | case1 pr = record { zc = {!!} ;  chain-mono = {!!} ; f-total = {!!} } where
              ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain zc0) ax )
-             ... | case1 is-sup = ? where -- x is a sup of zc 1
+             ... | case1 is-sup = {!!} where -- x is a sup of zc 1
                 sup0 : SUP A (chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → (chain zc0) ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -600,12 +600,12 @@
                 x=sup = sym &iso 
                 chain0 = chain zc0
                 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
-                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ? )
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< {!!} )
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
-             ... | case2 ¬x=sup =  ?
-         ... | no  ¬ox  = record { zc = zcu ; chain-mono = sz03 ; f-total = ? } where
+             ... | case2 ¬x=sup =  {!!}
+         ... | no  ¬ox  = record { zc = zcu ; chain-mono = sz03 ; f-total = {!!} } where
               pzc :  (z : Ordinal) → z o< x → ZChain A y f z
               pzc z z<x = ind f mf ay z (λ w w<px → zc (prev z z<x) (o<→≤ w<px) )
               Uz⊆A : {z : Ordinal} → UZFChain A f x y pzc z ∨ FClosure A f y z → odef A z
@@ -618,12 +618,20 @@
                  ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
               zcu1 : { z : Ordinal } → z o≤ x → ZChain1 y f z
               zcu1 {z} z≤x with  osuc-≡< z≤x
-              ... | case1 z=x = record { zc = ? ; chain-mono = ? ; f-total = ? }
+              ... | case1 z=x = record { zc = {!!} ; chain-mono = {!!} ; f-total = {!!} }
               ... | case2 z<x = prev z z<x 
               zcu : { z : Ordinal } → z o≤ x → ZChain A y f z
-              zcu {z} z≤x = ind f mf ay z (λ w w<px → zc (zcu1 z≤x ) (o<→≤ w<px) )
+              zcu {z} z≤x with osuc-≡< z≤x                                                                                                                                
+              ... | case1 z=x = record { chain = Uz }
+              ... | case2 z<x = ind f mf ay z (λ w w<px → zc (prev z z<x ) (o<→≤ w<px) )
               sz03 : {a b : Ordinal} → (a≤b : a o≤ b) → (b≤x : b o≤ x ) →  chain (zcu {a} (OrdTrans a≤b b≤x))  ⊆' chain (zcu b≤x ) 
-              sz03 = ?
+              sz03 {a} {b} a≤b b≤x {i} ai with osuc-≡< (OrdTrans a≤b b≤x) | osuc-≡< b≤x
+              ... | case1 a=x | case1 b=x = {!!}
+              ... | case1 a=x | case2 b<x = ⊥-elim ( osuc-< (subst (λ k → k o< osuc b ) a=x a≤b) b<x )
+              ... | case2 a<x | case1 b=x = case1 record { u = a ; u<x = a<x ; chain∋z = subst (λ k → odef k i) {!!} ai  } where
+                  sz04 : {!!}
+                  sz04 = {!!}
+              ... | case2 a<x | case2 b<x = {!!}
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM