Lemma isabgrop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) : isabgrop opp → isabgrop (binop_weq_bck H opp). Proof. intro is. split. apply isgrop_weq_bck, (pr1 is). apply iscomm_weq_bck, (pr2 is). Defined.