Lemma invstruct_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (is : ismonoidop opp) : invstruct opp is → invstruct (binop_weq_fwd H opp) (ismonoidop_weq_fwd H opp is). Proof. intro inv. exists (λ y : Y, H (pr1 inv (invmap H y))). apply isinv_weq_fwd, (pr2 inv). Defined.