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

diff -r 64b243e501b2 -r 250e52f15f43 src/cardinal.agda
--- a/src/cardinal.agda	Mon Jun 26 09:03:12 2023 +0900
+++ b/src/cardinal.agda	Mon Jun 26 10:42:16 2023 +0900
@@ -70,13 +70,23 @@
       ay : odef (* a) y
       x=fy : x ≡ i→ iab _ ay
 
-Image : { a b : Ordinal } → Injection a b → HOD
-Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
+Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD
+Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
     im00 : {x : Ordinal } → IsImage a b iab x → x o< b
     im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso 
          (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) )
 
-Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image iab ⊆ * b 
+record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where
+   field
+      ax : odef (* a) x
+      x=fy : y ≡ i→ iab x ax
+
+InverseImage : {a : Ordinal} ( b : Ordinal ) → Injection a b → (y : Ordinal ) → HOD
+InverseImage {a} b iab y = record { od = record { def = λ x → IsInverseImage a b iab x y } ; odmax = & (* a) ; <odmax = im00  } where
+    im00 : {x : Ordinal } → IsInverseImage a b iab x y → x o< & (* a)
+    im00 {x} record { ax = ax ; x=fy = x=fy } = odef< ax
+
+Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b 
 Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay)
 
 _=c=_ : ( A B : HOD ) → Set n
@@ -142,19 +152,22 @@
             be02 : CN x
             be02 = subst (λ k → odef k x) *iso lt
 
-      fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a  f) ))
+      fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f) ))
       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 : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (& UC) (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⁻¹ = ?
+            g⁻¹ : ( x : Ordinal) → odef (* b) x → Ordinal
+            g⁻¹ x bx = fba _ bx  
+            a∋g⁻¹ : ( x : Ordinal) → (bx : odef (* b) x ) → odef (* a) (g⁻¹ x bx ) 
+            a∋g⁻¹ x bx = a∋fba x bx
+            is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → g⁻¹ (fba x ?) ?  ≡ x
+            is-g⁻¹ {x} bx = begin
+                ? ≡⟨ ? ⟩
+                ? ∎ where
+                   open ≡-Reasoning
             be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? }  where 
                 be02 : CN x
                 be02 = subst (λ k → odef k x) *iso lt
@@ -165,13 +178,13 @@
                 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 0 {x} (a-g ax ¬ib) = record { y = ?
+                    ; ay = subst (λ k → odef k ? ) (sym *iso) record { i = 0 ; gfix = a-g ? ?} ; x=fy = ? }
                 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 : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f))) (& UC) 
       gU = ?
 
       -- Injection (b - a) b