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

changeset 1429:5f22e830e460

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 18:19:34 +0900
parents a2b59bbe5eef
children f2125be6fec1
files src/cardinal.agda
diffstat 1 files changed, 35 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 16:47:37 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 18:19:34 2023 +0900
@@ -208,6 +208,11 @@
       be16 {x} lt with subst (λ k → odef k x) *iso lt
       ... | ⟪ ax , ncn ⟫ = nimg ax ncn
 
+      cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (x₁ : ¬ gfImage x) 
+          → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 (subst (λ k → odef k x) (sym *iso) ⟪ ax , x₁ ⟫)) 
+               (be16 (subst (λ k → odef k x) (sym *iso) ⟪ ax , x₁ ⟫)))
+      cc11-case2 {x} ax gfi = ?
+
       be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x
       be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = be18 } where
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
@@ -218,19 +223,29 @@
               be19 : odef (* b) (g⁻¹ (be15 lt) (be16 lt))
               be19 = b∋g⁻¹ (be15 lt) (be16 lt)
               be18 : odef a-UC x →  ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 lt) (be16 lt))
-              be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be13 (UC∋gf ay) ) where
-                   be13 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x
-                   be13 = begin
+              be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be113 (UC∋gf ay) ) where
+                   be113 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x
+                   be113 = begin
                       fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy)  ⟩
                       fba (g⁻¹ (be15 lt) (be16 lt)) be19 ≡⟨ g⁻¹-iso (be15 lt) (be16 lt) ⟩
                       x ∎ where open ≡-Reasoning
           be18 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → g⁻¹ (be15 ltx) (be16 ltx) ≡ g⁻¹ (be15 lty) (be16 lty) → x ≡ y
           be18 = ?
 
+      be13 : (x : Ordinal) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
+      be13 x lt = fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt ))
+
+      be60 : {b x : Ordinal} → (bx : odef (* b) x) → (ncn : ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) ) 
+           → odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
+      be60 {b} {x} bx ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
+
+      cc10-case2 : {x : Ordinal } → (bx : odef (* b) x )
+         → (x₁ : ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x )
+         → ¬ gfImage (be13 x (subst (λ k → odef k x) (sym *iso) (be60 bx x₁)))
+      cc10-case2 = ?
+
       be11 : Injection  (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC)   -- g x
       be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where
-          be13 : (x : Ordinal) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
-          be13 x lt = fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt ))
           be14 : (x : Ordinal) (lt : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& a-UC)) (be13 x lt)
           be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be25 ⟫ where
               be26 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)
@@ -352,9 +367,15 @@
       h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) →  (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x))
           → Ordinal
       h⁻¹ {x} bx ( case1 cn)  = Uf x (subst (λ k → odef k x) (sym *iso) cn)                    --   x ≡ f y
-      h⁻¹ {x} bx ( case2 ncn) = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where     -- ¬ x ≡ f y
-           be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-           be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
+      h⁻¹ {x} bx ( case2 ncn) = i→ be11 x (subst (λ k → odef k x ) (sym *iso) (be60 bx ncn) ) -- ¬ x ≡ f y
+
+      cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → CC0 (h⁻¹ bx cc1 ) 
+      cc10 {x} bx (case1 x₁) = case1 (subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) x₁)))
+      cc10 {x} bx (case2 x₁) = case2 (cc10-case2 bx x₁ ) 
+
+      cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x) → CC1 (h ax cc0 ) 
+      cc11 {x} bx (case1 x₁) = case1 (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁)))
+      cc11 {x} bx (case2 x₁) = case2 (cc11-case2 bx x₁)
 
       be70 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef (* b) (h lt or )
       be70 x ax ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where    -- make the same condition for Uf
@@ -372,9 +393,7 @@
            be03 : (cn : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* a) (Uf x cn )
            be03 cn with subst (λ k → odef k x ) *iso cn
            ... | record { y = y ; ay = ay ; x=fy = x=fy } = UC⊆a ay
-      be71 x bx ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) be60) ))   where
-           be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-           be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
+      be71 x bx ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) (be60 bx ncn)) ))   
 
       be71-1 :  (x : Ordinal) (bx : odef (* b) x) 
              → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) 
@@ -384,14 +403,6 @@
       be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) 
       be70-1 = ?
 
-      cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → CC0 (h⁻¹ bx cc1 ) 
-      cc10 {x} bx (case1 x₁) = case1 ?
-      cc10 {x} bx (case2 x₁) = ?
-
-      cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x) → CC1 (h ax cc0 ) 
-      cc11 {x} bx (case1 x₁) = case1 (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁)))
-      cc11 {x} bx (case2 x₁) = ?
-
       be74 : (x : Ordinal) (ax : odef (* a) x) → odef (* b) (h ax (cc0 x))
       be74 x ax with cc0 x
       ... | case1 lt1 = ?
@@ -410,8 +421,9 @@
       ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
-      be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = UC-iso11 x be76 
-                  (subst (λ k → odef k (IsImage.y (subst (λ k → odef k x) *iso be76))) (sym *iso) be77 ) where
+      be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = ? where
+      -- UC-iso11 x be76 
+      --            (subst (λ k → odef k (IsImage.y (subst (λ k → odef k x) *iso be76))) (sym *iso) be77 ) where
            be76 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
            be76 = subst (λ k → odef k x) (sym *iso) x₁
            be78 : y ≡ IsImage.y (subst (λ k → odef k x) *iso be76)
@@ -423,18 +435,8 @@
       ... | 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  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 = ?
+      ... | case2 c2 with nimg (a∋fba x bx) (subst (λ k → gfImage (fba x k) → ⊥) ? c2 )
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym (inject g _ _ ? ? ?)
 
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x