定义“依赖类型”模函子

如何生成依赖类型的函子(因为缺少更好的术语)?我想做如下事情:

Module Type Element.
  ...
End Element.

Module Wrapper (E : Element).
  ...
End Wrapper.

Module DepentlyTypedFunctor (E : Element) (W : Wrapper E).
  ...
End DepentlyTypedFunctor.

最后一个定义不起作用,我想我正在寻找正确的语法,如果可能的话。我做这种定义的动机是在里面定义定理 DependentlyTypedFunctor 对所有人都有用 Wrappers 包含的任何实例 Element ,类似于定义向量的定理, forall (E : Element) (W : Wrapper E), some_proposition E W 。