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

comparison src/cardinal.agda @ 1397:94baa4bdfd7d

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 Wed, 28 Jun 2023 07:34:01 +0900
parents ac854f01352b
children d586aaa9b0bd
comparison
equal deleted inserted replaced
1396:ac854f01352b 1397:94baa4bdfd7d
300 bx = subst (λ k → odef (* b) k ) (sym x=fix) ( b∋fab ix (a∋gfImage (CN.i be04) (CN.gfix be04))) 300 bx = subst (λ k → odef (* b) k ) (sym x=fix) ( b∋fab ix (a∋gfImage (CN.i be04) (CN.gfix be04)))
301 by : odef (* b) y 301 by : odef (* b) y
302 by = subst (λ k → odef (* b) k ) (sym x=fiy) ( b∋fab iy (a∋gfImage (CN.i be06) (CN.gfix be06))) 302 by = subst (λ k → odef (* b) k ) (sym x=fiy) ( b∋fab iy (a∋gfImage (CN.i be06) (CN.gfix be06)))
303 303
304 UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x 304 UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x
305 UC-iso0 x cx = ? 305 UC-iso0 x cx = ? where
306 be02 : CN x
307 be02 = subst (λ k → odef k x) *iso cx
308 be03 : i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x
309 be03 with CN.i be02 | CN.gfix be02 | iB fU x cx
310 ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb
311 ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? -- fba (fab x _) _ = x
312 be03 | suc i | next-gf s ix | cb with subst (λ k → odef k (fab x _) ) *iso cb
313 ... | record { y = y ; ay = ay ; x=fy = x=fy } = ?
306 314
307 UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → i→ fU ( i→ Uf x cx ) (iB Uf x cx) ≡ x 315 UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → i→ fU ( i→ Uf x cx ) (iB Uf x cx) ≡ x
308 UC-iso1 = ? 316 UC-iso1 = ?
309 317
310 318