Lemma isunit_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) : isunit opp x0 → isunit (binop_weq_fwd H opp) (H x0). Proof. intro is. split. apply islunit_weq_fwd, (pr1 is). apply isrunit_weq_fwd, (pr2 is). Defined.