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.
Unsafebecause it uses a postulate. I'm reasonably sure that you cannot proveFalsewith it.FC's, FMC'sandFSMC'sare all just extensions of eachother, but they can share no code if we define them independently.extralets us essentially add constructors later on. If this turns out later to be too complicated, we can also make it different types.