# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688174343 -32400
# Node ID ee40c5b5cefed55c017b9c4c0e09352501a6b17a
# Parent  cdfe297f9a7930e9c009074eb281207c699d05ad
...

diff -r cdfe297f9a79 -r ee40c5b5cefe src/cardinal.agda
--- a/src/cardinal.agda	Sat Jul 01 09:18:05 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 10:19:03 2023 +0900
@@ -391,8 +391,11 @@
       ... | case1 lt1 = ?
       ... | case2 lt1 = ?
 
-      ImageInject : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
-      ImageInject {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))
+      fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx)
+      fba-image {x} bx = record { y = _ ; ay = bx ; x=fy = refl }
+
+      ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
+      ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
       be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = UC-iso11 x be76 
@@ -400,7 +403,7 @@
            be76 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
            be76 = subst (λ k → odef k x) (sym *iso) x₁
            be78 : y ≡ IsImage.y (subst (λ k → odef k x) *iso be76)
-           be78 = ImageInject x₁ (subst (λ k → odef k x) *iso be76)
+           be78 = ImageUnique x₁ (subst (λ k → odef k x) *iso be76)
            be77 : odef UC (IsImage.y (subst (λ k → odef k x) *iso be76))
            be77 = subst₂ (λ j k → odef j k ) *iso be78 ay 
       be72 x bx (case2 x₁)  with cc10 bx (case2 x₁)
@@ -408,9 +411,27 @@
       ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) 
          = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 
              ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) })
-      ... | case2 c2 = trans ? (g⁻¹-iso ? ?) where
-            be76 : g⁻¹ (a∋fba x bx) record { y = IsImage.y ?  ; ay = ? ;  x=fy = ? } ≡ x
-            be76 = a-UC-iso1 x (subst (λ k → odef k x) (sym *iso) ⟪ bx , (subst (λ k → ¬ odef k x) (sym *iso) x₁)  ⟫ )
+      ... | case2 c2  = be80 where
+           be79 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )) x
+           be79 = subst (λ k → odef k x) (sym *iso) ⟪ bx , subst (λ k → odef k x → ⊥) (sym *iso) x₁ ⟫
+           bx1 : odef (* b) x
+           bx1 = proj1 (subst (λ k → odef k x) *iso be79)
+           be77 : odef (Image b g) (fba x (proj1 (subst (λ k → odef k x) *iso be79)) )
+           be77 = nimg (a∋fba x (proj1 (subst (λ k → odef k x) *iso be79))) c2
+           be80 : g⁻¹ ? ? ≡ x
+           be80 = ?
+
+      -- with ODC.p∨¬p O ( IsImage b a g (fba x bx ))
+      -- ... | case1 (img @ record { y = y ; ay = ay ; x=fy = x=fy }) = trans (ImageUnique ? ? ) (sym ( inject g _ _ bx ay x=fy )) where
+      --      be79 : odef (* b) x
+      --      be79 = proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) 
+      --             ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))
+      --      be78 : odef (Image b g) ?
+      --      be78 = nimg (a∋fba ? ?) c2
+      --      be77 : odef (Image b g) (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) 
+      --             ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫)))) 
+      --      be77 = nimg (a∋fba ? ?) c2
+      -- ... | case2 ¬img = ?
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x
       be73 x ax (case1 x₁) with cc11 ax (case1 x₁)