proposition: Lemma isrinv_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) (inv : Y → Y) : isrinv opp x0 inv → isrinv (binop_weq_bck H opp) (invmap H x0) (λ y : X, invmap H (inv (H y))).
proof: Proof. intros is y. unfold binop_weq_bck. apply maponpaths. refine (pathscomp0 _ (is _)). apply (maponpaths (opp _)). apply homotweqinvweq. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions