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

comparison src/zorn.agda @ 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
comparison
equal deleted inserted replaced
874:852bdf4a2df3 875:7f03e1d24961
421 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 421 , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫
422 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) )) 422 ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
423 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt ) 423 ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
424 424
425 csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 425 csupf1 : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b)
426 csupf1 {b} sb<z = ⟪ ? , ch-is-sup (supf b) ? record { fcy<sup = fcy<sup ? ; order = ? ; supu=u = ? } (init ? ? ) ⟫ 426 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
427 b<z : b o< z
428 b<z = supf-inject0 supf-mono ( ordtrans<-≤ sb<z (x≤supfx z) )
429 asb : odef A (supf b)
430 asb = supf∈A (o<→≤ b<z)
427 431
428 -- ordering is not proved here but in ZChain1 432 -- ordering is not proved here but in ZChain1
429 433
430 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 434 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
431 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 435 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where