Generalise ExactSequence.v to a pointed wildcat with kernels

[Alizter]

We should generalise ExactSequence.v to work on any pointed wildcat with kernels which will generalise many things from pType to abelian categories, groups, spectra etc.

It might also be worth checking if things like the 5-lemma hold in such generality.

[Alizter]

Just to add, obviously the 5-lemma doesn't literally hold in this case because it talks about monos and epis. The variant where we use the exactness characterization of monos and epis called the "short five lemma" should hold. (We even have it in the library for Ab).