--- a/src/CCCSets.agda	Tue Mar 30 17:58:55 2021 +0900
+++ b/src/CCCSets.agda	Tue Mar 30 20:22:20 2021 +0900
@@ -160,9 +160,13 @@
         tchar {a} {b} m mono y with lem (image m y )
         ... | case1 t = true
         ... | case2 f = false
-
+        open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+        img-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) (t : image m y') → s ≅ t
+        img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
+            with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
+        ... | refl = HE.refl
         image-iso : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → (i0 i1 : image m y ) → i0 ≡ i1
-        image-iso = {!!}
+        image-iso {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1)
         tchar¬Img : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → tchar m mono y ≡ false → ¬ image m y
         tchar¬Img  m mono y eq im with lem (image m y) 
         ... | case2 n  = n im