Lemma invstruct_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (is : ismonoidop opp) : invstruct opp is → invstruct (binop_weq_bck H opp) (ismonoidop_weq_bck H opp is). Proof. intro inv. exists (λ y : X, invmap H (pr1 inv (H y))). apply isinv_weq_bck, (pr2 inv). Defined.