Add (uni)setoids and setoid morphisms

Just spitting some stuff out.

By the way, do we need the `hom-trunc` constraint on the setoid definition? It seems like it technically should be there, but I do not know if it is important for practical purposes.