Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1421:cdfe297f9a79
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jul 2023 09:18:05 +0900 |
| parents | 836bcc102a2c |
| children | ee40c5b5cefe |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 10 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Sat Jul 01 07:44:45 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 09:18:05 2023 +0900 @@ -404,12 +404,19 @@ be77 : odef UC (IsImage.y (subst (λ k → odef k x) *iso be76)) be77 = subst₂ (λ j k → odef j k ) *iso be78 ay be72 x bx (case2 x₁) with cc10 bx (case2 x₁) - ... | case1 c1 = ⊥-elim ( x₁ ? ) - ... | case2 c2 = trans ? (a-UC-iso1 x ? ) + ... | case1 (a-g ax ¬ib) = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = (fba-eq refl) } ) + ... | 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 = trans ? (g⁻¹-iso ? ?) where + be76 : g⁻¹ (a∋fba x bx) record { y = IsImage.y ? ; ay = ? ; x=fy = ? } ≡ x + be76 = a-UC-iso1 x (subst (λ k → odef k x) (sym *iso) ⟪ bx , (subst (λ k → ¬ odef k x) (sym *iso) x₁) ⟫ ) be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) → h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x be73 x ax (case1 x₁) with cc11 ax (case1 x₁) - ... | case1 c1 = trans ? (UC-iso0 x (subst (λ k → odef k x) (sym *iso) ? )) + ... | case1 c1 = ? where + be76 : IsImage.y (subst (λ k → odef k (fU x (subst (λ k₁ → odef k₁ x) (sym *iso) x₁))) *iso (be04 (subst (λ k → odef k x) (sym *iso) x₁))) ≡ x + be76 = UC-iso0 x (subst (λ k → odef k x) (sym *iso) x₁ ) ... | case2 c2 = ? be73 x ax (case2 x₁) with cc11 ax (case2 x₁) ... | case1 c1 = ⊥-elim ( x₁ ? )