Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1425:a0e8df81a466
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jul 2023 16:03:42 +0900 |
| parents | a444ea176011 |
| children | 800218d431dc |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Sat Jul 01 15:50:34 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 16:03:42 2023 +0900 @@ -423,7 +423,7 @@ ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) }) - ... | case2 c2 = a-UC-iso11 x be76 be77 where + ... | case2 c2 = trans ? ( a-UC-iso11 x be76 be77) where be76 : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x be76 = subst (λ k → odef k x) (sym *iso) ⟪ bx , (λ lt → subst (λ k → odef k x → ⊥) (sym *iso) x₁ lt ) ⟫ be77 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76)))