Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1397:94baa4bdfd7d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2023 07:34:01 +0900 |
| parents | ac854f01352b |
| children | d586aaa9b0bd |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 9 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Tue Jun 27 18:38:41 2023 +0900 +++ b/src/cardinal.agda Wed Jun 28 07:34:01 2023 +0900 @@ -302,7 +302,15 @@ by = subst (λ k → odef (* b) k ) (sym x=fiy) ( b∋fab iy (a∋gfImage (CN.i be06) (CN.gfix be06))) UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x - UC-iso0 x cx = ? + UC-iso0 x cx = ? where + be02 : CN x + be02 = subst (λ k → odef k x) *iso cx + be03 : i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x + be03 with CN.i be02 | CN.gfix be02 | iB fU x cx + ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? -- fba (fab x _) _ = x + be03 | suc i | next-gf s ix | cb with subst (λ k → odef k (fab x _) ) *iso cb + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? 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 UC-iso1 = ?