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

changeset 1424:a444ea176011

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 15:50:34 +0900
parents 77a3de21ee50
children a0e8df81a466
files src/cardinal.agda
diffstat 1 files changed, 28 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 14:26:20 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 15:50:34 2023 +0900
@@ -197,14 +197,19 @@
       g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a g (fba x bx) )  → g⁻¹ (a∋fba x bx) nc0  ≡ x
       g⁻¹-iso1 {x} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) 
 
+      g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a g x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0'
+      g⁻¹-eq {x} ax ax' {record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ }} {record { y = y ; ay = ay ; x=fy = x=fy }} 
+           = inject g _ _ ay₁ ay (trans (sym x=fy₁) x=fy )
+
+      be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
+      be15 {x} lt with subst (λ k → odef k x) *iso lt
+      ... | ⟪ ax , ncn ⟫ = ax
+      be16 : {x : Ordinal } → odef (* (& a-UC)) x →  IsImage b a g x 
+      be16 {x} lt with subst (λ k → odef k x) *iso lt
+      ... | ⟪ ax , ncn ⟫ = nimg ax ncn
+
       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
-          be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
-          be15 {x} lt with subst (λ k → odef k x) *iso lt
-          ... | ⟪ ax , ncn ⟫ = ax
-          be16 : {x : Ordinal } → odef (* (& a-UC)) x →  IsImage b a g x 
-          be16 {x} lt with subst (λ k → odef k x) *iso lt
-          ... | ⟪ ax , ncn ⟫ = nimg ax ncn
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
           be17 x lt = subst ( λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) (sym *iso) ⟪ be19 , 
                  (λ img → be18 be14 (subst (λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) *iso img) )  ⟫  where
@@ -227,14 +232,14 @@
           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 )) , be15 ⟫ where
-              be16 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)
-              be16 = proj2 ( subst (λ k → odef k x) (*iso) lt )
-              be15 : ¬ gfImage (be13 x lt)
-              be15 cn with cn
+          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)
+              be26 = proj2 ( subst (λ k → odef k x) (*iso) lt )
+              be25 : ¬ gfImage (be13 x lt)
+              be25 cn with cn
               ... | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } )
               ... | next-gf  record { y = y ; ay = ay ; x=fy = x=fy } t 
-                   = ⊥-elim (be16 (subst (λ k → odef k x) (sym *iso) record { y = y 
+                   = ⊥-elim (be26 (subst (λ k → odef k x) (sym *iso) record { y = y 
                       ; ay = subst (λ k → odef k y) (sym *iso) t ; x=fy = be17 })) where
                   be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) t))
                   be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl)
@@ -250,7 +255,9 @@
       a-UC-iso11 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) 
            → (ib : odef (* (& a-UC)) (fba x ( proj1 ( subst (λ k → odef k x) (*iso) cx )) ))
            → i→ be10 ( i→ be11 x cx ) ib  ≡ x
-      a-UC-iso11 x cx ib = trans ? (a-UC-iso1 x cx)
+      a-UC-iso11 x cx ib with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) )
+      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy )
+      ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl })
 
       --   C n → f (C n) 
       fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
@@ -416,21 +423,14 @@
       ... | 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  = ? where -- a-UC-iso11 x be79 (subst (λ k → odef k (fba x (proj1 (subst (λ k₁ → odef k₁ x) *iso be79 )  ))) (sym *iso) be77 ) where
-           be79 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )) x
-           be79 = proj1 (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) ⟪ bx , subst (λ k → odef k x → ⊥) (sym *iso) x₁ ⟫))
-           bx1 : odef (* b) x
-           bx1 = proj1 (subst (λ k → odef k x) *iso be79)
-           be77 : odef a-UC (fba x bx1 )
-           be77 = subst (λ k → odef k (fba x bx)) *iso (subst (λ k → odef k (fba x bx)) (sym *iso) ⟪ bx , subst (λ k → odef k (fba x bx) → ⊥) (sym *iso) x₁ ⟫)
-           be80 : odef (* (& a-UC)) (fba x bx1 )
-           be80 = 
-                  (subst (λ k → odef 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)
-              ⟪ 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  = a-UC-iso11 x  be76 be77 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)) , ? ⟫
+
+
       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