Lemma isinv_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) (inv : Y → Y) : isinv opp x0 inv → isinv (binop_weq_bck H opp) (invmap H x0) (λ y : X, invmap H (inv (H y))). Proof. intro is. split. apply islinv_weq_bck, (pr1 is). apply isrinv_weq_bck, (pr2 is). Defined.