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

changeset 1428:a2b59bbe5eef

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:47:37 +0900
parents 2134c62fdc30
children 5f22e830e460
files src/cardinal.agda
diffstat 1 files changed, 12 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 16:13:27 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 16:47:37 2023 +0900
@@ -423,16 +423,18 @@
       ... | 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 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 ) ⟫
-           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₁ ⟫))) , ? ⟫)) , c2 ⟫
+      ... | case2 c2  with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) 
+                 (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) ))) )
+      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) )) ? ? )
+      ... | case2 nimg = ?
+      -- =  trans (g⁻¹-eq _ (be15 be51) {_} {be16 be51}) be50  where
+      --     be52 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x 
+      --     be52 = subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫
+      --     be51 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52)))
+      --     be51 = subst (λ k → odef k (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52)))) (sym *iso) 
+      --       ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52)) , ? ⟫
+      --     be50 : g⁻¹ (be15 be51) (be16 be51) ≡ x
+      --     be50 = ?
 
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x