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

changeset 875:7f03e1d24961

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, 17 Sep 2022 12:53:51 +0900
parents 852bdf4a2df3
children 23dcb59d1231
files src/zorn.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Sep 17 10:11:54 2022 +0900
+++ b/src/zorn.agda	Sat Sep 17 12:53:51 2022 +0900
@@ -423,7 +423,11 @@
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
    csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
-   csupf1 {b} sb<z = ⟪ ? , ch-is-sup (supf b) ? record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init ? ? ) ⟫
+   csupf1 {b} sb<z = ⟪ asb , ch-is-sup (supf b) sb<z record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? }  (init (subst (λ k → odef A k) ? asb)  (supf-idem) ) ⟫ where
+        b<z : b o< z
+        b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z (x≤supfx z) )
+        asb : odef A (supf b)
+        asb = supf∈A (o<→≤ b<z)
 
    -- ordering is not proved here but in ZChain1