proposition: Lemma isapropisgrop {X : hSet} (opp : binop X) : isaprop (isgrop opp).
proof: Proof. apply (isofhleveltotal2 1). - apply isapropismonoidop. - apply isapropinvstruct. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions