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

changeset 1395:e39c2bffb86e

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 10:50:07 +0900
parents 873924d06ff7
children ac854f01352b
files src/cardinal.agda
diffstat 1 files changed, 13 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Tue Jun 27 09:20:55 2023 +0900
+++ b/src/cardinal.agda	Tue Jun 27 10:50:07 2023 +0900
@@ -244,9 +244,20 @@
                         
 
           Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f))) (& UC) 
-          Uf = record { i→ = ? ; iB = λ x lt →  ? ; inject = ? } where
+          Uf = record { i→ = be00 ; iB = be01 ; inject = ? } where
                  be00 : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
-                 be00 = ?
+                 be00 x lt with subst (λ k → odef k x ) *iso lt
+                 ... | record { y = y ; ay = ay ; x=fy = x=fy } = fba x (subst (λ k → odef (* b) k ) (trans fab-refl (sym x=fy)) (b∋fab y (UC⊆a ay) ) )
+                 be01 : (x : Ordinal) → (lt : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ) → odef (* (& UC)) (be00 x lt)
+                 be01 x lt with subst (λ k → odef k x) *iso lt
+                 ... | record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ (λ j k → odef j k ) (sym *iso) fba-refl be02 where
+                      be04 : CN y
+                      be04 = subst (λ k → odef k y) *iso ay
+                      be02 : CN (be00 x lt)
+                      be02 = record { i = suc (CN.i be04 ) ; gfix = next-gf (CN.gfix be04) record { y = ? ; ay = ? ; x=fy = ?  } }
+                      be03 : x ≡ fab y (a∋gfImage (CN.i be04) (CN.gfix be04))
+                      be03 = x=fy
+ 
 
     be00 : OrdBijection a b
     be00 with trio< a b