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

comparison src/zorn.agda @ 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
comparison
equal deleted inserted replaced
921:c0cf2b383064 922:620c2f3440f5
1314 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1314 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1315 uz01 = ? 1315 uz01 = ?
1316 1316
1317 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → SUP A (UnionZF f mf ay ) 1317 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → SUP A (UnionZF f mf ay )
1318 -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay) 1318 -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay)
1319 sp0 f mf {x} ay = ? -- 1319 sp0 f mf {x} ay = ? -- supP ? ? ?
1320
1321 sp00 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
1322 (zc : ZChain A f mf ay x ) → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
1323 sp00 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
1324 ztotal : IsTotalOrderSet (ZChain.chain zc)
1325 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1326 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1327 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
1320 1328
1321 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) 1329 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )
1322 → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 )) 1330 → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 ))
1323 fixpoint f mf = z14 where 1331 fixpoint f mf = z14 where
1324 chain = UnionZF f mf as0 1332 chain = UnionZF f mf as0