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

changeset 1430:f2125be6fec1

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 19:37:54 +0900
parents 5f22e830e460
children 052f0fca7799
files src/cardinal.agda
diffstat 1 files changed, 44 insertions(+), 61 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 18:19:34 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 19:37:54 2023 +0900
@@ -124,8 +124,8 @@
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })
      = record { 
-         fun←  = λ x lt → h lt (cc0 x)
-       ; fun→  = λ x lt → h⁻¹ lt (cc1 x)
+         fun←  = λ x lt → h lt ?
+       ; fun→  = λ x lt → h⁻¹ lt ?
        ; funB  = be74
        ; funA  = be75
        ; fiso← = λ x lt → be72 x lt (cc11 (a∋fba x lt) (cc20 lt))
@@ -158,6 +158,7 @@
 
       aucimg : {x : Ordinal } → (cx : odef (* (& a-UC)) x ) → IsImage b a g x
       aucimg {x} cx with subst (λ k → odef k x ) *iso cx
+
       ... | ⟪ ax , ncn ⟫ = nimg ax ncn
 
       --  UC ⊆ * a
@@ -208,10 +209,17 @@
       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 = ?
+      nimg1 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) → IsImage b a g x
+      nimg1 {x} ax ncn = nimg ax ncn
+
+      cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) 
+          → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ ax (nimg ax ncn))
+      cc11-case2 {x} 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⁻¹ ax (nimg ax ncn) ) (b∋g⁻¹ ax (nimg ax ncn) ) ≡⟨ g⁻¹-iso ax (nimg ax ncn) ⟩
+                      x ∎ where open ≡-Reasoning
 
       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
@@ -330,22 +338,22 @@
          → (ux : odef (* (& UC)) (Uf x cx)) → fU ( Uf x cx ) ux  ≡ x
       UC-iso11 x cx ux = subst (λ k → fU (Uf x cx) k ≡ x) ( HE.≅-to-≡ ( ∋-irr {* (& UC)} {_} (be08 cx) ux)) (UC-iso1 x cx)
 
-      CC0 : (x : Ordinal) → Set n
-      CC0 x =  gfImage x ∨ (¬ gfImage x) 
+      CC0 : (x : Ordinal) → (bx : odef (* a) x)  → Set n
+      CC0 x ax =  gfImage x ∨ (¬ gfImage x) 
 
-      CC1 : (x : Ordinal) → Set n
-      CC1 x =  odef (Image (& UC) (Injection-⊆ UC⊆a f)) x ∨ (¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) 
+      CC1 : (x : Ordinal) → (bx : odef (* b) x) → Set n
+      CC1 x bx =  gfImage (fba x bx) ∨  (¬ gfImage (fba x bx) )
 
-      cc0 : (x : Ordinal) → CC0 x
+      cc0 : (x : Ordinal) → CC0 x ?
       cc0 x = ODC.p∨¬p O (gfImage x) 
 
-      cc1 : (x : Ordinal) → CC1 x
-      cc1 x = ODC.p∨¬p O (odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) 
+      cc1 : (x : Ordinal) → (bx : odef (* b) x) → CC1 x ?
+      cc1 x bx = ODC.p∨¬p O (gfImage (fba x bx) )
 
-      cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt )
+      cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) ?
       cc20 = ?
 
-      cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt )
+      cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) ?
       cc21 = ?
 
       --
@@ -360,22 +368,21 @@
       --
       --  otherwise not strict positive on gfImage error will happen
 
-      h : {x : Ordinal } → (ax : odef (* a) x) → gfImage x ∨ (¬ gfImage x) → Ordinal
+      h : {x : Ordinal } → (ax : odef (* a) x) → CC0 x ax → Ordinal
       h {x} ax (case1 cn)  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
-      h {x} ax (case2 ncn) = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) 
+      h {x} ax (case2 ncn) = g⁻¹ ax (nimg ax ncn)
+
+      h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → CC1 x bx → Ordinal
+      h⁻¹ {x} bx ( case1 cn)  = Uf x ?                    --   x ≡ f y
+      h⁻¹ {x} bx ( case2 ncn) = fba x bx
 
-      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 bx ncn) ) -- ¬ x ≡ f y
+      cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x bx) → 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 ? ) 
 
-      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₁)
+      cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ax) → CC1 (h ax cc0 ) ?
+      cc11 {x} ax (case1 x₁) = case1 ? -- (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁)))
+      cc11 {x} ax (case2 x₁) = case2 ? -- (cc11-case2 ax 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
@@ -384,11 +391,11 @@
            ... | a-g ax ¬ib = b∋fab x ax
            ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = b∋fab x
                  (subst (odef (* a)) (sym x=fy) (a∋fba (fab y ay) (b∋fab y ay)))
-      be70 x ax ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) 
+      be70 x ax ( case2 ncn ) = ? -- proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) 
 
       be71 :  (x : Ordinal) (bx : odef (* b) x) 
              → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   ))
-             → odef (* a) (h⁻¹ bx or )
+             → odef (* a) (h⁻¹ bx ? )
       be71  x bx ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where
            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
@@ -397,7 +404,7 @@
 
       be71-1 :  (x : Ordinal) (bx : odef (* b) x) 
              → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) 
-             → gfImage (h⁻¹ bx (case1 or) )
+             → gfImage (h⁻¹ bx (case1 ? ) )
       be71-1 x bx cn = subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) cn))  
 
       be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) 
@@ -409,10 +416,8 @@
       ... | case2 lt1 with iB be10 ? ?
       ... | t = ?
 
-      be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx (cc1 x))
-      be75 x lt with cc1 x
-      ... | case1 lt1 = ?
-      ... | case2 lt1 = ?
+      be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx ? )
+      be75 x lt  = ?
 
       fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx)
       fba-image {x} bx = record { y = _ ; ay = bx ; x=fy = refl }
@@ -420,34 +425,12 @@
       ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
       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 })) = ? 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)
-           be78 = ImageUnique x₁ (subst (λ k → odef k x) *iso be76)
-           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 (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 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 _ _ ? ? ?)
+      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x bx) →  h (be71 x bx ? ) (cc10 bx ? ) ≡ x
+      be72 x bx = ?
 
 
-      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 ? be76 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₁ ? )
-      ... | case2 c2 = trans ? (a-UC-iso0 x ? )
+      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ax ) →  h⁻¹ (be70 x ax cc0) ? ≡ x
+      be73 x ax (case1 x₁) = ?
 
 
 _c<_ : ( A B : HOD ) → Set n