Lemma isinv_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) (inv : X → X) : isinv opp x0 inv → isinv (binop_weq_fwd H opp) (H x0) (λ y : Y, H (inv (invmap H y))). Proof. intro is. split. apply islinv_weq_fwd, (pr1 is). apply isrinv_weq_fwd, (pr2 is). Defined.