--- a/src/CCCSets.agda	Sat Mar 27 22:52:43 2021 +0900
+++ b/src/CCCSets.agda	Sun Mar 28 08:11:58 2021 +0900
@@ -113,8 +113,14 @@
     case1 : a → a ∨ b
     case2 : b → a ∨ b
 
-data char {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where
-   isChar : (x : b ) → char m (m x) 
+--
+-- m : b → a determins a subset of a as an image
+-- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x.
+--   so tchar m mono and ker (tchar m mono) is Iso.
+--   Finding (x : b) from (y : a) is non constructive. Assuming LEM of image.
+--
+data image {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where
+   isImage : (x : b ) → image m (m x) 
 
 topos : {c : Level } → ({ c : Level} →  (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
 topos {c} lem = record {
@@ -128,14 +134,17 @@
          }
     } where
 --
+-- In Sets, equalizers exist as
 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
 --     elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
+-- m have to be isomorphic to ker (char m).
+--
 --                   i          ○ b
 --   ker (char m)  ----→ b -----------→ 1
 --       |         ←---- |              |
---       |           j   |m             | ⊤   char m : a → Ω = {1,⊥}
---       |   e           ↓    char m    ↓     if y : a ≡ m (∃ x : b) → 1
---       +-------------→ a -----------→ Ω     else         ⊥
+--       |           j   |m             | ⊤   char m : a → Ω = {true,false}
+--       |   e           ↓    char m    ↓     if y : a ≡ m (∃ x : b) → true  ( data char )
+--       +-------------→ a -----------→ Ω     else         false
 --                             h
 --
         tker   : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ])
@@ -144,29 +153,29 @@
               ; equalizer = λ e → equ e
               ; isEqualizer = SetsIsEqualizer _ _ _ _ }
         tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c}
-        tchar {a} {b} m mono y with lem (char m y )
+        tchar {a} {b} m mono y with lem (image m y )
         ... | case1 t = true
         ... | case2 f = false
         isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Bool (tchar m mono)  (λ _ → true )) → equ e )
         isol {a} {b} m mono  = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; iso→  = {!!} ; iso←  = {!!} } ; iso≈L = {!!} } where
           b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
-          b→s x with lem (char m (m x) )
+          b→s x with lem (image m (m x) )
           ... | case1 x₁ = bs1 x₁ refl where
-             bs1 : {y : a } → char m y → y ≡ m x  → sequ a Bool (λ y → tchar m mono y) (λ _ → true)
-             bs1 (isChar x) eq = elem (m x) {!!}
-          ... | case2 n = ⊥-elim (n (isChar x))
+             bs1 : {y : a } → image m y → y ≡ m x  → sequ a Bool (λ y → tchar m mono y) (λ _ → true)
+             bs1 (isImage x) eq = elem (m x) {!!}
+          ... | case2 n = ⊥-elim (n (isImage x))
           b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
-          b←s (elem y eq) with lem (char m y)
-          ... | case1 (isChar x) = x
+          b←s (elem y eq) with lem (image m y)
+          ... | case1 (isImage x) = x
           ... | case2 t = ⊥-elim ( ¬f≡t eq )
         imequ   : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ])
         imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
         uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
                tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
-        uniq {a} {b} h m mono y with h y  | lem (char (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
+        uniq {a} {b} h m mono y with h y  | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
         ... | true | case1 x | record { eq = eq1 } = eq1 
         ... | true | case2 x | record { eq = eq1 } = {!!}
-        ... | false | case1 x | record { eq = eq1 }  = {!!}
+        ... | false | case1 (isImage (elem x eq)) | record { eq = eq1 } = {!!}
         ... | false | case2 x | record { eq = eq1 }  = eq1