WIP: quotients

[marcosh]

No description provided.

[marcosh]

@andrek-sbox some questions just to get a better understanding:

• would it be useful/wise/feasible to define quotients for a general category and only for types and functions as it is now?
• is the UnsageQuotient really unsafe? Is it just that a proof of safety is postulated or is there the possibility of doing real harm?
• what is the exact role of extra in FreeQuotients?

[andrek-sbox]

• I'm not aware of any good way of defining quotients for general categories. While there are ways to define something like an equivalence relation in a more general setting, I'm not aware of a definitive way of doing so. Another way would be with coequalizers, but I'm not sure if this would be usable in practice.
• it's just called Unsafe because it uses a postulate. I'm reasonably sure that you cannot prove False with it.
• It is used to extend the datatypes later. Note that FC's, FMC's and FSMC's are all just extensions of eachother, but they can share no code if we define them independently. extra lets us essentially add constructors later on. If this turns out later to be too complicated, we can also make it different types.