Constructions vs Instances

[anuyts]

Within the Cubical.Categories module, one distinguishes between Instances and Constructions. The only distinguishing criterion that I can think of is that constructions are instances with "many" parameters and instances are constructions with "few" parameters. This seems rather arbitrary, so I would suggest to merge these modules in the interest of finding stuff more easily.

[maxsnew]

I agree with this. It is the only part of the library where this distinction is made, e.g., AbGroup has direct product under Instances. And right now it's not even consistent as Functors is under Instances.

I propose we just move everything under Constructions to Instances. It's a breaking change but easy to fix downstream.

[anuyts]

Seems we also have to do this for Cubical.Categories.Displayed.[Constructions/Instances].