AFAIK using dependent records-as-modules in a simpler MLTT-based type systems is tricky, because singleton types (aka. 'manifest fields') usually depend on equality reflection. Has anyone applied cubical type theory to the problem of first class module systems?
Conversation
Also aware of the other tricky issues around combining subtyping in dependent types? Generative modules might also be problematic… given that these are kind of 'effectful', which is always a bit fun?