--- a/src/CCCGraph.agda	Sat Mar 06 16:50:47 2021 +0900
+++ b/src/CCCGraph.agda	Sat Mar 06 19:11:01 2021 +0900
@@ -95,17 +95,42 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
+data II  {c : Level } : Set c where
+     true : II
+     false : II
 
--- tooos : {c : Level } → Topos (Sets {c}) sets
--- tooos  = record {
---          Ω = {!!}
---       ;  ⊤ = {!!}
---       ;  Ker = {!!}
---       ;  char = {!!}
---       ;  isTopos = record {
---  
---          }
---     }
+data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where
+     isTrue : (x : a ) → f x ≡ true → Tker f
+
+topos : {c : Level } → Topos (Sets {c}) sets
+topos  = record {
+         Ω = II
+      ;  ⊤ = λ _ → true
+      ;  Ker = tker
+      ;  char = tchar
+      ;  isTopos = record {
+                 char-uniqueness  = {!!}
+              ;  ker-iso = {!!}
+         }
+    } where
+        etker : {a : Obj Sets} (h : Hom Sets a II) → Hom Sets ( Tker h ) a
+        etker h (isTrue x eq) = x
+        e-eq : {a : Obj Sets} (h : Hom Sets a II) →  Sets [ Sets [ h o etker h ] ≈ Sets [ Sets [ (λ _ → true) o CCC.○ sets a ] o etker h ] ]
+        e-eq h  = {!!}
+        tker   : {a : Obj Sets} (h : Hom Sets a II) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
+        tker {a} h = record {
+                equalizer-c = Tker h
+              ; equalizer = etker h
+              ; isEqualizer = record {
+                      fe=ge = e-eq h 
+                   ;  k = {!!}
+                   ;  ek=h = {!!}
+                   ;  uniqueness = {!!}
+              }
+          }
+        tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a II
+        tchar {a} {b} m mono x = true
+
 
 
 open import graph
@@ -501,14 +526,12 @@
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
        c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs g} 
            → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       --- Hom (cat c) (cobj f a) (cobj f (atom b))
-      ------ g  : Obj Grph
-      ------ c  : Obj Cart
-      ------ a  : Objs g
-      ------ b  : V g
-      ------ f  : Hom Grph g (uobj c)
-      ------ y  : fobj g a → (y₁ : vertex g) → C g y₁ b
-       c-map {g} {c} {a} {atom b} f y = ?
+       --- from x to b chain. but we forgot how we come here ...
+       c-map {g} {c} {atom x} {atom b} f y = {!!}
+       --- next three cases cannot be negerated
+       c-map {g} {c} {⊤} {atom b} f y = {!!}
+       c-map {g} {c} {a ∧ a₁} {atom b} f y = {!!}
+       c-map {g} {c} {a <= a₁} {atom b} f y = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ k → proj₁ (z k))) (c-map f (λ k → proj₂ (z k)))
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ k → x (proj₁ k)  (proj₂ k)))