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

changeset 1393:c67ecdf89e77

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 Tue, 27 Jun 2023 08:48:41 +0900
parents 8645a167d76b
children 873924d06ff7
files src/bijection.agda src/cardinal.agda
diffstat 2 files changed, 59 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Mon Jun 26 15:52:14 2023 +0900
+++ b/src/bijection.agda	Tue Jun 27 08:48:41 2023 +0900
@@ -57,6 +57,13 @@
 -- famous diagnostic function
 --
 
+--   1 1 0 1 0 ...
+--   0 1 0 1 0 ...
+--   1 0 0 1 0 ...
+--   1 1 1 1 0 ...
+
+--   0 0 1 0 1 ...  diag
+
 diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
@@ -82,7 +89,7 @@
 b-iso b = fiso← b _
 
 --
--- ℕ <=> ℕ + 1
+-- ℕ <=> ℕ + 1    (infinite hotel)
 --
 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
 to1 {n} {R} b = record {
--- a/src/cardinal.agda	Mon Jun 26 15:52:14 2023 +0900
+++ b/src/cardinal.agda	Tue Jun 27 08:48:41 2023 +0900
@@ -116,6 +116,10 @@
 Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx) 
         ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq  } 
 
+Injection-∙ : {a b c : Ordinal } → Injection a b → Injection b c → Injection a c
+Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax)
+        ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq)   } 
+
 
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 Bernstein {a} {b} iab iba = be00 where
@@ -150,6 +154,9 @@
 
           UC : HOD
           UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
+
+          b-UC : HOD
+          b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt)  }
           
           --  UC ⊆ * a
           --     f : UC → Image f UC    is injection
@@ -160,6 +167,24 @@
                 be02 : CN x
                 be02 = subst (λ k → odef k x) *iso lt
 
+          b-UC⊆b : * (& b-UC) ⊆ * b
+          b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
+
+          be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
+          be10 = record { i→ = be12 ; iB = ? ; inject = ? } where
+              be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
+              be12 x lt = i→ g x (proj1 be02) where
+                    be02 : odef (* b) x ∧ ( ¬ CN x )
+                    be02 = subst (λ k → odef k x) *iso lt
+
+          be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
+          be11 = record { i→ = be13 ; iB = ? ; inject = ? } where
+              be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal
+              be13 x lt with subst (λ k → odef k x) *iso lt 
+              ... | record { y = y ; ay = ay ; x=fy = x=fy } = y where -- x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay))
+                    be02 : odef (* b) y ∧ ( ¬ CN y )
+                    be02 = subst (λ k → odef k y) *iso ay
+
           open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
           fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x}  → fab x ax ≡ fab x ax1
@@ -168,7 +193,7 @@
           fUC = & (Image (& UC) {b} (Injection-⊆ UC⊆a  f) )
           --   C n → f (C n) 
           fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f) ))
-          fU = record { i→ = be00 ; iB = λ x lt →  be50 x lt ; inject = ? } where
+          fU = record { i→ = be00 ; iB = λ x lt →  be50 x lt ; inject = be51 } where
                 be00 : (x : Ordinal) (lt : odef (* (& UC)) x) → Ordinal
                 be00 x lt = be03 where
                     be02 : CN x
@@ -188,8 +213,32 @@
                     ... | zero | a-g {x} ax ¬ib = record { y = x ; ay = lt1 ; x=fy = fab-refl } 
                     ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy } = record { y = _ ; ay = lt1 ; x=fy = fab-refl } 
 
+                be51 : (x y : Ordinal) (ltx : odef (* (& UC)) x) (lty : odef (* (& UC)) y) → be00 x ltx ≡ be00 y lty → x ≡ y
+                be51 x y ltx lty eq = be04 where
+                    be0x : CN x
+                    be0x = subst (λ k → odef k x) *iso ltx
+                    be0y : CN y
+                    be0y = subst (λ k → odef k y) *iso lty
+                    be04 : x ≡ y
+                    be04 with CN.i be0x | CN.gfix be0x | CN.i be0y | CN.gfix be0y 
+                    ... | 0 | a-g ax ¬ib | 0 | a-g ax₁ ¬ib₁ = fab-inject _ _ ax ax₁ eq 
+                    ... | 0 | a-g ax ¬ib | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where
+                        ay : odef (* a) y
+                        ay = a∋gfImage (suc j) (next-gf gfyi iy )
+                    ... | suc i | next-gf gfxi ix | 0 | a-g ay ¬ib = fab-inject _ _ ax ay eq where
+                        ax : odef (* a) x
+                        ax = a∋gfImage (suc i) (next-gf gfxi ix )
+                    ... | suc i | next-gf gfxi ix | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where
+                        ax : odef (* a) x
+                        ax = a∋gfImage (suc i) (next-gf gfxi ix )
+                        ay : odef (* a) y
+                        ay = a∋gfImage (suc j) (next-gf gfyi iy )
+                        
+
           Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f))) (& UC) 
-          Uf = ?
+          Uf = record { i→ = ? ; iB = λ x lt →  ? ; inject = ? } where
+                 be00 : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
+                 be00 = ?
 
     be00 : OrdBijection a b
     be00 with trio< a b