proposition: Lemma islunit_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) : islunit opp x0 → islunit (binop_weq_fwd H opp) (H x0).
proof: Proof. intros is y. unfold binop_weq_fwd. refine (pathscomp0 (maponpaths _ _) _). - refine (pathscomp0 (maponpaths (λ x, opp x _) _) _). + apply homotinvweqweq. + apply is. - apply homotweqinvweq. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions