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

changeset 1388:2e53a8e6fa5f

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 Sun, 25 Jun 2023 18:32:07 +0900
parents 003424a36fed
children 242bba9c82bf
files src/cardinal.agda
diffstat 1 files changed, 33 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sun Jun 25 15:58:16 2023 +0900
+++ b/src/cardinal.agda	Sun Jun 25 18:32:07 2023 +0900
@@ -102,27 +102,49 @@
 
 open Data.Nat
 
+Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
+Injection-⊆ = ?
+
 Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧  Injection b a → Injection (b - a) b ∧  Injection b (b - a) 
 Bernstein1 {a} {b} a<b ⟪ f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject } , g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject } ⟫ 
     = ⟪ record { i→ = f0 ; iB = b∋f0 ; inject = f0-inject } , record { i→ = f1 ; iB = b∋f1 ; inject = f1-inject } ⟫ where
 
-      C : ℕ → HOD
-      gf : (i : ℕ) → Injection (& (C i)) a
-      gf 0 = record { i→ = λ x cx  → fba x ?  ; iB = ? ; inject = ? }
-      gf (suc i) = record { i→ = be00 ; iB = ? ; inject = ? } where 
-          be00 : (x : Ordinal) → odef (* (& (C (suc i)))) x → Ordinal
-          be00 x lt with subst (λ k → odef k x) *iso lt | inspect C (suc i)
-          ... | t | record { eq = eq1 }  = ?
-      C 0 = (* a) ＼ Image g
-      C (suc i) = Image {& (C i)} {a} (gf i) 
+      gf : Injection a a
+      gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
+         ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } 
+
+      data gfImage : (i : ℕ) (x : Ordinal) → Set n where
+          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
+          next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→  (ix : IsImage a a gf x) → gfImage (suc i) x
+
+      a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
+      a∋gfImage 0 {x} (a-g ax ¬ib) = ax
+      a∋gfImage (suc i) {x} (next-gf lt record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
+
+      C : ℕ → HOD                                               --  Image {& (C i)} {a} (gf i)  does not work
+      C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } 
 
       record CN (x : Ordinal) : Set n where
           field 
              i : ℕ
-             cn=x : & (C i) ≡ x
+             gfix : gfImage i x
 
       UC : HOD
-      UC = record { od = record { def = λ x → CN x } ; odmax = a ; <odmax = ? }
+      UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
+      
+      --  UC ⊆ * a
+      --     f : UC → Image f UC    is injection
+      --     g : Image f UC → UC    is injection
+
+      UC⊆a : * (& UC) ⊆ * a
+      UC⊆a {x} lt with subst (λ k → odef k x) *iso lt
+      ... | t = ?
+
+      fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f) ))
+      fU = ?
+
+      gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f))) (& UC) 
+      gU = ?
 
       -- Injection (b - a) b 
       f0 : (x : Ordinal) → odef (* (b - a)) x → Ordinal