--- a/src/zorn.agda	Sun Jun 05 12:49:48 2022 +0900
+++ b/src/zorn.agda	Mon Jun 06 07:47:45 2022 +0900
@@ -249,24 +249,32 @@
           → 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} → ZC A f s → FClosure A f s x → ZC A f x
-   zc-sup : {s x : Ordinal} → ZC A f s → * s < * x  → ZC A f x
+   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 = ? 
-    ; chain⊆A = ? 
-    ; chain∋x = ? 
-    ; initial = ? 
-    ; f-total = ? 
-    ; f-next = ? 
-    ; f-immediate = ? 
-    ; is-max = ? 
-    ; fc∨sup = ?
+      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