# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687830607 -32400
# Node ID e39c2bffb86ed0212b2a89a601017d93fe65cfc4
# Parent  873924d06ff7c385ef73c7ac9063bc4f12dc8b19
...

diff -r 873924d06ff7 -r e39c2bffb86e src/cardinal.agda
--- 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