# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687737792 -32400
# Node ID 64b243e501b2a04a44b6804358197badd3982631
# Parent  242bba9c82bf6c2adaf76ce709d6baa206f83e7a
...

diff -r 242bba9c82bf -r 64b243e501b2 src/cardinal.agda
--- a/src/cardinal.agda	Mon Jun 26 07:10:12 2023 +0900
+++ b/src/cardinal.agda	Mon Jun 26 09:03:12 2023 +0900
@@ -143,30 +143,33 @@
             be02 = subst (λ k → odef k x) *iso lt
 
       fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f) ))
-      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
+      fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt →  be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where
+            be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a  f) x
+            be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (Injection-⊆ UC⊆a f)))) x
+            be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt )
+            be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt))
+            be21 = ?
+            g⁻¹ : { x : Ordinal} → odef (* b) x → Ordinal
+            g⁻¹ = ?
+            a∋g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → odef (* a) (g⁻¹ bx ) 
+            a∋g⁻¹ = ?
+            is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → x ≡ fab (g⁻¹ bx ) (a∋g⁻¹ bx)
+            is-g⁻¹ = ?
+            be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? }  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)) ? )
+                be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi )
                 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)
+                be14 (suc i) {x} (next-gf lt _) = fba   ( fab (be14 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 (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
+                be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi) 
+                be16 0 {x} (a-g ax ¬ib) = record { y = g⁻¹ (b∋fab x ax)  
+                    ; ay = subst (λ k → odef k ( g⁻¹ (b∋fab x ax))) (sym *iso) record { i = 0 ; gfix = a-g ? ? } ; x=fy = is-g⁻¹ ? }
+                be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? }
+                be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02)) 
+                be11 = be16 _ (CN.gfix be02)
 
       gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f))) (& UC) 
       gU = ?