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

changeset 679:55767354aee7

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:37:32 +0900
parents fca33c0e9a88
children b27501ac4f4a
files src/zorn.agda
diffstat 1 files changed, 5 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jul 09 17:31:25 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 17:37:32 2022 +0900
@@ -262,24 +262,17 @@
    field
       psup :  Ordinal → Ordinal 
       psup<z : (x : Ordinal ) →   psup x o< & A 
-      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
+      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≤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
-ChainF A f mf {y} ay z zc = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup (zc (& A)) x ) x } 
-         ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
-
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ChainF A f mf ay z zc0 
+   chain = ZChain1.chainf (zc0 (& A)) z ?
    field
       chain-mono : (px py : Ordinal) → (px≤py : px o≤ py ) (y≤x : py o≤ z ) → (w : Ordinal ) 
-          → ChainF A f mf ay px zc0  ⊆' ChainF A f mf ay py zc0 
+          → ZChain1.chainf (zc0 (& A)) px  ? ⊆' ZChain1.chainf (zc0 (& A)) py ?
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
@@ -488,7 +481,7 @@
               --
               px = Oprev.oprev op
               supf : Ordinal → HOD
-              supf x =  ChainF A f mf ay x zc0 
+              supf x =  ? -- ChainF A f mf ay x zc0 
               -- zc : ZChain A f mf ay zc0 (Oprev.oprev op)
               -- zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
               px<x : px o< x