I think I'm getting the hang of universe polymorphism. Quite tedious though.
@lyxia I have once built myself an *intuition* that would help me predict whenever a given declaration would fail or require the polymorphic attribute... was a bit better than throwing a coin, but I think I’ve lost it now ):
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !