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

changeset 1427:2134c62fdc30

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 Sat, 01 Jul 2023 16:13:27 +0900
parents 800218d431dc
children a2b59bbe5eef
files src/cardinal.agda
diffstat 1 files changed, 4 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 16:03:54 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 16:13:27 2023 +0900
@@ -423,20 +423,16 @@
       ... | 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 ? ( a-UC-iso11 x  be76 be77) where
+      ... | case2 c2  =  a-UC-iso11 x  be76 be78 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)))
-           be77 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)) )) (sym *iso) 
-               ⟪ a∋fba x (proj1 (subst (λ k → odef k x) *iso be76)) , ? ⟫
-           be78 : fba x (proj1 (subst (λ k → odef k x) *iso be76)) p
+           be78 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76)))
+           be78 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)))) 
               (sym *iso) ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x
                     (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso)
                        ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso)
                 ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso)
-                   ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , (λ cn →
-                   cardinal.be25 O fab b∋fab fab-inject fba a∋fba fba-inject x (subst (λ k → OD.def (od k) x) (sym *iso)
-                    ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) cn | cn) ⟫)) , c2 ⟫))
+                   ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , ? ⟫)) , c2 ⟫
 
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x