Add kernels, cokernels, normal, conormal

[ScriptRaccoon]

While working on #75 it became clear that some proofs that subobject classifiers or quotient object classifiers are missing are actually coming from the fact that the categories are not normal or conormal*.

So to clarify these relationships, this PR adds normal and conormal categories, and includes their relationship to mono-regular and epi-regular categories. In this context it also makes sense to add kernels and cokernels and include their relationship to equalizers and coequalizers. The 4 new properties have been decided for all categories in the database. They also now appear in the definition of an abelian category. This has been done mostly automatically with the implications. For example, kernels and cokernels have been decided automatically for all categories except for Rel, where a quick proof confirms that they exist.

*The proofs for some missing regular subobject classifiers (and the dual notion) could be made more concise by adding yet another notion, being "regular normal", meaning that every regular monomorphism is a kernel. (For example, the current proof that CMon does not have a regular quotient subobject classifier is partly formal.) But for now I will not add this, as it seems to be a bit too niche and has no official name either.