proposition: Lemma isasetbinopiso (X Y : setwithbinop) : isaset (binopiso X Y).
proof: Proof. use isaset_total2. - use isaset_total2. + use impred_isaset. intros t. use setproperty. + intros x. use isasetaprop. use isapropisweq. - intros w. use isasetaprop. use isapropisbinopfun. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions