Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1419:2da55d442e4f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jul 2023 06:19:03 +0900 |
| parents | 51956de51455 |
| children | 836bcc102a2c |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 8 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Fri Jun 30 21:57:16 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 06:19:03 2023 +0900 @@ -388,9 +388,14 @@ ... | case2 lt1 = ? be72 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) → h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x - be72 x bx (case1 x₁) with cc10 bx (case1 x₁) - ... | case1 c1 = ? -- trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁)) - ... | case2 c2 = ⊥-elim ( c2 ? ) + be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = subst (λ k → fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) k ≡ x) + ? be76 where + be77 : odef (* (& UC)) (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) ≅ be08 (subst (λ k → odef k x) (sym *iso) x₁) + be77 = ? + be76 : fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) (be08 (subst (λ k → odef k x) (sym *iso) x₁)) ≡ x + be76 = UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁) + -- ... | case1 c1 = ? -- trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁)) + -- ... | case2 c2 = ⊥-elim ( c2 ? ) be72 x bx (case2 x₁) with cc10 bx (case2 x₁) ... | case1 c1 = ⊥-elim ( x₁ ? ) ... | case2 c2 = trans ? (a-UC-iso1 x ? )