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

changeset 922:620c2f3440f5

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 Mon, 17 Oct 2022 11:29:37 +0900
parents c0cf2b383064
children 85f6238a38db
files src/zorn.agda
diffstat 1 files changed, 9 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 17 10:32:31 2022 +0900
+++ b/src/zorn.agda	Mon Oct 17 11:29:37 2022 +0900
@@ -1316,7 +1316,15 @@
 
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  → SUP A (UnionZF f mf ay )
      -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay)
-     sp0 f mf {x} ay = ? -- 
+     sp0 f mf {x} ay = ? -- supP ? ? ?
+
+     sp00 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         (zc : ZChain A f mf ay x ) → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
+     sp00 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
+        ztotal : IsTotalOrderSet (ZChain.chain zc) 
+        ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  
             → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 ))