--- a/CCCGraph.agda	Thu May 02 11:54:09 2019 +0900
+++ b/CCCGraph.agda	Fri May 03 17:11:33 2019 +0900
@@ -97,7 +97,7 @@
 module ccc-from-graph where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
-   open import discrete
+   open import graph
    open graphtocat 
 
    open Graph
@@ -265,10 +265,10 @@
      ; associative =  λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h}
    }} 
 
-open import discrete
+open import graph
 open Graph
 
-record GMap {v v' w w' : Level} (x : Graph {v} {v'} ) (y : Graph {w} {w'} ) : Set (suc (v ⊔ w) ⊔  v' ⊔ w' ) where
+record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (suc (v ⊔ v') ) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)