proposition: Lemma isrunit_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) : isrunit opp x0 → isrunit (binop_weq_bck H opp) (invmap H x0).
proof: Proof. intros is y. unfold binop_weq_bck. refine (pathscomp0 (maponpaths _ _) _). - refine (pathscomp0 (maponpaths (opp _) _) _). + apply homotweqinvweq. + apply is. - apply homotinvweqweq. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions