proposition: Lemma isapropisabgrop {X : hSet} (opp : binop X) : isaprop (isabgrop opp).
proof: Proof. apply (isofhleveldirprod 1). apply isapropisgrop. apply isapropiscomm. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions