Add the category of semigroups

[ScriptRaccoon]

This PR adds the category SemiGrp of semigroups and decides all of its properties.

To prove that it does not have a NNO, a lemma has been added that connects NNOs with distributivity, a partial converse of the implication countably distributive => NNO.

[ScriptRaccoon]

@dschepler Can we adapt the proof that Mon has not effective cocongruences for SemiGrp?

[dschepler]

@dschepler Can we adapt the proof that Mon has not effective cocongruences for SemiGrp?

I think so. In that case, $\langle p \mid p^2 = p \rangle$ would become the terminal semigroup, and $\langle p, q \mid p^2 = p, q^2 = q, pq = q, qp = p \rangle$ would become a two-element semigroup where the operation just returns the second argument.