Lemma islunit_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) : islunit opp x0 → islunit (binop_weq_bck H opp) (invmap H x0). Proof. intros is y. unfold binop_weq_bck. refine (maponpaths _ _ @ _). - refine (maponpaths (λ x, opp x _) _ @ _). + apply homotweqinvweq. + apply is. - apply homotinvweqweq. Defined.