Fail to do unification for dependent path types

#1

I tried to model the Category of groups by dependent path type,
but found the following errors:

#2

Problem is that when you say val dom: Group = x, you’re erasing that underlying type you’re interested in