# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657355485 -32400
# Node ID fca33c0e9a884a2f0191c954e2ca9ea885b9a037
# Parent  be3eb95d50d917ca3626348f9b5081fc841773dd
...

diff -r be3eb95d50d9 -r fca33c0e9a88 src/zorn.agda
--- a/src/zorn.agda	Sat Jul 09 17:23:41 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 17:31:25 2022 +0900
@@ -262,9 +262,11 @@
    field
       psup :  Ordinal → Ordinal 
       psup<z : (x : Ordinal ) →   psup x o< & A 
-      chainf : (x : Ordinal) → x o< z  →  HOD
-      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x x<z ) w → Chain A f mf ay (psup x ) w 
-      psup-mono : (x y : Ordinal) → x o≤ y → chainf x ? ⊆' chainf y ? 
+      is-chain : (x w : Ordinal) → (x≤z : x o≤ z) →  Chain A f mf ay (psup x ) w 
+   chainf : (x : Ordinal) → x o≤ z  →  HOD
+   chainf x x≤z = record { od = record { def = λ w → is-chain x w ? } ; odmax = ? ; <odmax = ? }
+   field
+      psup-mono : (x y : Ordinal) → (x≤z : x o≤ z ) → chainf x x≤z ⊆' chainf z ? 
 
 ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 
      → (z : Ordinal) →  ( ( x : Ordinal ) → ZChain1 A f mf ay x ) →  HOD