Multisetoid attempt

I'm posting this here mostly for feedback.

1. I am not sure it is correct; is what I have defined a generalized multisetoid?

2. Is this the way you want laws formulated? (Since we are specialized on `Set` for the underlying machinery, I rewrote the laws to extensionally equivalent versions that we can actually do in Agda without using needing e-categories to define endofunctors and monads on `Set`.)