Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 678:fca33c0e9a88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jul 2022 17:31:25 +0900
parents be3eb95d50d9
children 55767354aee7
files src/zorn.agda
diffstat 1 files changed, 5 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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