--- a/CCChom.agda	Fri Apr 26 18:24:07 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 19:50:27 2019 +0900
@@ -637,7 +637,9 @@
    fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ z → smap G x ( k z ) where
        k : fobj a → fobj {G} c 
        k z = fmap f z
-   fmap {G} {a} {b} (next (id b) f) = fmap f
+   fmap {G} {a} {b} (next (id b) f) = λ z → k z where
+       k : fobj a → fobj {G} b
+       k z = fmap f z
    fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
    fmap {G} {a} {b} (next {a} {x ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
        k : fobj a → fobj x /\ fobj y  
@@ -648,9 +650,9 @@
    fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (k z))(  proj₂ (k z)) where
        k :  fobj a →  (fobj y → fobj x) /\ fobj y
        k z = fmap f z
-   fmap {G} {a} {b} (next {.a} {c} (_・_ {c} {d} {b} f g) h) =  λ z → fmap ( next f (id d)) ( fmap (next g (id c )) ( fmap h z ))
+   fmap {G} {a} {b} (next (f ・ g ) h) = {!!} -- λ z → fmap (next f (next g h )) z 
    fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z ,  fmap (next g h) z)
-   fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
+   fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = {!!} -- λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
 
    CS : {G : SM } → Functor (DX G) (Sets {Level.zero})
    FObj CS a  = fobj a