Lemma isgrop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) : isgrop opp → isgrop (binop_weq_fwd H opp). Proof. intro is. use tpair. - apply ismonoidop_weq_fwd, (pr1 is). - apply invstruct_weq_fwd, (pr2 is). Defined.