# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658364837 -32400
# Node ID 4a3ba4ad59d45d198f3605d55900a3df1be63ff7
# Parent  dc208a885e0c5d77d1318398ac752f7792931e4a
...

diff -r dc208a885e0c -r 4a3ba4ad59d4 src/zorn.agda
--- a/src/zorn.agda	Thu Jul 21 09:40:16 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 09:53:57 2022 +0900
@@ -365,8 +365,8 @@
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
-     -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
+ChainP-next A f mf {y} ay supf {x} {z} cp = record { y<s = ChainP.y<s cp ; supfu=u  = ChainP.supfu=u cp  
+     ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -461,7 +461,7 @@
                 m08 with proj2 m06
                 ... | record { u = _ ; u<x = u<x ; uchain = ch-init .(HasPrev.y has-prev) fc } = 
                           ch-init (f (HasPrev.y has-prev)) (fsuc _ fc) 
-                ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup ? (fsuc _ fc) 
+                ... | record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } = ch-is-sup (ChainP-next A f mf ay _ is-sup) (fsuc _ fc) 
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? ; sup=u = ? ; order = ? } where