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

changeset 686:b854c1f07873

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 Sun, 10 Jul 2022 10:08:59 +0900
parents 6826883cfbf8
children af1d69eb429e
files src/zorn.agda
diffstat 1 files changed, 13 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jul 10 08:41:01 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 10:08:59 2022 +0900
@@ -500,24 +500,33 @@
           pzc z z<x = prev z z<x
           UZ : HOD
           UZ = UnionCF A x pchainf
+          total-UZ : IsTotalOrderSet UZ
+          total-UZ {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 (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
+                                            (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
           usup : SUP A UZ
-          usup = supP UZ ? ? 
+          usup = supP UZ (λ lt → proj1 lt) total-UZ 
           sc4 :  ZChain1 A f mf ay x
           sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 ; psup-mono = sc0 }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? x z
-            ... | yes _ = ?
+            ... | yes _ = & (SUP.sup usup)
             ... | no z<x = ZChain1.psup (pzc z (o¬≤→< z<x)) z
             p≤z1 : (z : Ordinal ) → odef A (psup1 z)
             p≤z1 z with o≤? x z
-            ... | yes _  = ?
+            ... | yes _  = SUP.A∋maximal usup
             ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? x z
             ... | yes _  = UZ
             ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
             sc0 : (z : Ordinal) → z o≤ x → chainf1 z ⊆' chainf1 x
-            sc0 z = ?
+            sc0 z z≤x {i} lt with o≤? x z
+            ... | yes _ = ?
+            ... | no z<x = ? where -- subst (λ k → odef k i) refl sc1 where
+                sc1 : odef (ZChain1.chainf (pzc z (o¬≤→< z<x)) z) i
+                sc1 = ZChain1.psup-mono (pzc z (o¬≤→< z<x)) _ o≤-refl lt
             is-chain1 : ?
             is-chain1 = ?