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

changeset 1389:242bba9c82bf

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 Mon, 26 Jun 2023 07:10:12 +0900
parents 2e53a8e6fa5f
children 64b243e501b2
files src/cardinal.agda
diffstat 1 files changed, 29 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sun Jun 25 18:32:07 2023 +0900
+++ b/src/cardinal.agda	Mon Jun 26 07:10:12 2023 +0900
@@ -103,7 +103,8 @@
 open Data.Nat
 
 Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
-Injection-⊆ = ?
+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  } 
 
 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 } ⟫ 
@@ -137,11 +138,35 @@
       --     g : Image f UC → UC    is injection
 
       UC⊆a : * (& UC) ⊆ * a
-      UC⊆a {x} lt with subst (λ k → odef k x) *iso lt
-      ... | t = ?
+      UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02)  where
+            be02 : CN x
+            be02 = subst (λ k → odef k x) *iso lt
 
       fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f) ))
-      fU = ?
+      fU = record { i→ = be03 ; iB = be10 ; inject = ? } where
+            be03 : (x : Ordinal) → odef (* (& UC)) x → Ordinal
+            be03 x ucx = be04 _ (CN.gfix be02) where
+                be02 : CN x
+                be02 = subst (λ k → odef k x) *iso ucx
+                be04 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal
+                be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be04 i gfi )
+                be04 0 {x} (a-g ax ¬ib) = x
+                be04 (suc i) {x} (next-gf lt _) = fba   ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
+                be05 0 {x} (a-g ax ¬ib) = ax
+                be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
+            be10 : (x : Ordinal) (lt : odef (* (& UC)) x) →
+                odef (* (& (Image (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) (be03 x lt)
+            be10 x lt = subst (λ k → odef k (be03 x lt)) (sym *iso) be11 where
+                be02 : CN x
+                be02 = subst (λ k → odef k x) *iso lt
+                be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal
+                be15 : (i : ℕ) → {x : Ordinal } → gfImage i x → ( IsImage _ _ ((Injection-⊆ UC⊆a f)) ? )
+                be14 0 {x} (a-g ax ¬ib) = x
+                be14 (suc i) {x} (next-gf lt _) = fba   ( fab (be14 i lt) ? ) ( b∋fab _ ?)
+                be15 0 {x} (a-g ax ¬ib) = ?
+                be15 (suc i) {x} (next-gf ix ix₁) = ?
+                be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be03 x lt) 
+                be11 = be15 _ (CN.gfix be02)
 
       gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f))) (& UC) 
       gU = ?