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

changeset 1474:893954e484a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Bernstein fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Jun 2024 09:32:40 +0900
parents aca42b19db4c
children 6752e2ff4dc6
files src/cardinal.agda
diffstat 1 files changed, 39 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sun Jun 23 07:04:50 2024 +0900
+++ b/src/cardinal.agda	Sun Jun 23 09:32:40 2024 +0900
@@ -47,10 +47,10 @@
 
 import filter 
 
-open import Relation.Nullary 
 -- open import Relation.Binary hiding ( _⇔_ )
 open import Data.Empty 
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 import BAlgebra 
 
@@ -199,7 +199,7 @@
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b)
 Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) 
                   ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject })
-     = proj1 (==-bi (proj2 (==-bi (bi-∪  bi-UC  bi-fUC ? ? ) ) (==-sym b=fUC∨b-fUC)) ) (==-sym a=UC∨a-UC) 
+     = proj1 (==-bi (proj2 (==-bi (bi-∪  bi-UC  bi-fUC exUC exfUC ) ) (==-sym b=fUC∨b-fUC)) ) (==-sym a=UC∨a-UC) 
  where
       gf : Injection a a
       gf = record { i→ = λ x → g (f x ) ; iB = λ x ax → a∋g _ (b∋f x ax) 
@@ -252,8 +252,7 @@
       exUC : (UC ∩ a-UC) =h= od∅
       exUC = record { eq→ = be00 ; eq← = be01 } where
            be00 : {x : Ordinal} → odef (UC ∩ a-UC) x → odef od∅ x
-           be00 {x} ⟪ a-g ax₁ ¬ib , ⟪ ax , nuc ⟫ ⟫ = ?
-           be00 {x} ⟪ next-gf ix uc , ⟪ ax , nuc ⟫ ⟫ = ?
+           be00 {x} ⟪ uc , ⟪ ax , nuc ⟫ ⟫ = ⊥-elim ( nuc uc )
            be01 : {x : Ordinal} → odef od∅ x → odef (UC ∩ a-UC) x
            be01 {x} lt = ⊥-elim ( ¬x<0 lt )
 
@@ -279,16 +278,23 @@
            be01 {x} (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* b) k) (sym x=fy) ( b∋f y (a∋gfImage ay))
            be01 {x} (case2 ngfx) = proj1 ngfx
 
+      exfUC : (fUC ∩ b-fUC) =h= od∅
+      exfUC = record { eq→ = be00 ; eq← = be01 } where
+           be00 : {x : Ordinal} → odef (fUC ∩ b-fUC) x → odef od∅ x
+           be00 {x} ⟪ uc , ⟪ ax , nuc ⟫ ⟫ = ⊥-elim ( nuc uc )
+           be01 : {x : Ordinal} → odef od∅ x → odef (fUC ∩ b-fUC) x
+           be01 {x} lt = ⊥-elim ( ¬x<0 lt )
+
       nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a gi x
       nimg {x} ax ncn with p∨¬p  (IsImage b a gi x)
       ... | case1 img = img
       ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
 
-      f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ≡ f y 
-      f-cong {x} {x} {ax} {ax1} refl = refl 
+      -- f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ≡ f y 
+      -- f-cong {x} {x} {ax} {ax1} refl = refl 
 
-      g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x ≡ g y 
-      g-cong {x} {x} {bx} {bx1} refl = refl 
+      -- g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x ≡ g y 
+      -- g-cong {x} {x} {bx} {bx1} refl = refl 
 
       g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → Ordinal
       g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y
@@ -314,7 +320,7 @@
                                             (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) )  where
                be113 : g (f y )  ≡ x
                be113 = begin
-                    g (f y )  ≡⟨ g-cong (sym x=fy)  ⟩
+                    g (f y )  ≡⟨ cong g (sym x=fy)  ⟩
                     g y1 ≡⟨ sym (x=fy1) ⟩
                     x ∎ where open ≡-Reasoning
 
@@ -323,7 +329,7 @@
          → ¬ gfImage (g x )
       cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl }
       cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) 
-           = nix record { y = _ ; ay = gfy ; x=fy = inject gi _ _ bx (b∋f y (a∋gfImage gfy)) (trans x=fy (g-cong (f-cong refl))) }
+           = nix record { y = _ ; ay = gfy ; x=fy = inject gi _ _ bx (b∋f y (a∋gfImage gfy)) (trans x=fy (cong g (cong f refl))) }
 
       fU1 : (x : Ordinal) → odef UC x → Ordinal
       fU1 x gfx = f x 
@@ -335,13 +341,21 @@
       UC∋f⁻¹ {x} record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
       fU-iso1 : {x : Ordinal } → (lt : odef fUC x) → fU1 (f⁻¹ x lt) (UC∋f⁻¹ lt) ≡ x
-      fU-iso1 {x} record { y = y ; ay = (a-g ax ¬ib) ; x=fy = x=fy } = trans (f-cong refl) (sym x=fy) 
-      fU-iso1 {x} record { y = y ; ay = (next-gf record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ } ay) ; x=fy = x=fy } = trans (f-cong refl) (sym x=fy) 
+      fU-iso1 {x} record { y = y ; ay = (a-g ax ¬ib) ; x=fy = x=fy } = sym x=fy
+      fU-iso1 {x} record { y = y ; ay = (next-gf record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ } ay) ; x=fy = x=fy } = sym x=fy
 
       fU-iso0 : {x : Ordinal } → (lt : odef UC x) → f⁻¹ (fU1 x lt) record { y = _ ; ay = lt ; x=fy = refl } ≡ x
       fU-iso0 {x} (a-g ax ¬ib) = refl 
       fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = refl
 
+      f⁻¹-cong : (x y : Ordinal) → (isx : IsImage0 UC (* b) FA x) → (isy : IsImage0 UC (* b) FA y) → x ≡ y → f⁻¹ x isx ≡ f⁻¹ y isy
+      f⁻¹-cong x y isx@record { y = yx ; ay = ayx ; x=fy = x=fyx } isy@record { y = yy ; ay = ay ; x=fy = x=fy } eq = inject fi _ _ f01 f02 f00 where
+          f01 : odef (* a) (f⁻¹ x isx)
+          f01 = a∋gfImage (UC∋f⁻¹ isx)
+          f02 : odef (* a) (f⁻¹ y isy)
+          f02 = a∋gfImage (UC∋f⁻¹ isy)
+          f00 : f (f⁻¹ x isx) ≡ f (f⁻¹ y isy)  
+          f00 = trans ( fU-iso1 isx) (trans eq (sym (fU-iso1 isy)))
 
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
@@ -351,6 +365,8 @@
        ; funA  = λ x lt → UC∋f⁻¹ lt
        ; fiso→ = λ x lt → fU-iso1 lt
        ; fiso← = λ x lt → fU-iso0 lt
+       ; fcong→ = λ x y ax ay eq → cong f eq
+       ; fcong← = λ x y ax ay eq → f⁻¹-cong x y ax ay eq
        }
 
       b-FUC∋g⁻¹ : {x : Ordinal } → (lt : odef a-UC x )→ odef b-fUC (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) 
@@ -367,6 +383,13 @@
       fUC-iso0 {x} lt with nimg (proj1 lt) (proj2 lt)
       ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
+      g⁻¹-cong : (x y : Ordinal) → (ax : odef a-UC x) ( ay : odef a-UC y) 
+          → x ≡ y
+          → g⁻¹ (proj1 ax) (nimg (proj1 ax) (proj2 ax)) ≡ g⁻¹ (proj1 ay) (nimg (proj1 ay) (proj2 ay))
+      g⁻¹-cong x y ax ay eq = inject gi _ _ ( b∋g⁻¹ (proj1 ax) (nimg (proj1 ax) (proj2 ax))) ( b∋g⁻¹ (proj1 ay) (nimg (proj1 ay) (proj2 ay))) g00 where
+          g00 : g (g⁻¹ (proj1 ax) (nimg (proj1 ax) (proj2 ax))) ≡ g (g⁻¹ (proj1 ay) (nimg (proj1 ay) (proj2 ay)))
+          g00 = trans (fUC-iso0 ax) ( trans eq (sym (fUC-iso0 ay)))
+
       bi-fUC : HODBijection a-UC b-fUC
       bi-fUC = record { 
          fun→  = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))
@@ -375,6 +398,8 @@
        ; funA  = λ x lt → a-UC∋g lt
        ; fiso→ = λ x lt → fUC-iso1 lt
        ; fiso← = λ x lt → fUC-iso0 lt
+       ; fcong→ = λ x y ax ay eq → g⁻¹-cong x y ax ay eq
+       ; fcong← = λ x y ax ay eq → cong g eq
        }
 
 
@@ -400,11 +425,11 @@
 
 fun←cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  
     → x ≡ y  → fun← b x ax ≡ fun← b y ax1
-fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
+fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = fcong← b x x ax ax1 refl
      
 fun→cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef P x} {ax1 : odef P y}  
     → x ≡ y  → fun→ b x ax ≡ fun→ b y ax1
-fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 ))  
+fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = fcong→ b x x ax ax1 refl
      
 
 --    S