-- module
structure Map :=
  (M : Type -> Type)
  (K : Type)
  (V : Type)
  (read : K -> V)
  (insert : K -> V -> M K V -> M K V)

-- where refinement
definition int_map := { map | map.M = nat }

-- Another module
structure Hasher (T : Type) :=
  (Out : Type)
  ...

-- A functor
definition HashMapFunctor (T : Type) (H : Hasher T) : Map := ..