Definition trivialTorsorRightMultiplication (G:gr) : G ≃ ActionIso (trivialTorsor G) (trivialTorsor G). Proof. exists (trivialTorsorAuto G). simple refine (isweq_iso _ _ _ _). { intro f. exact (f (unel G)). } { intro g; simpl. exact (lunax _ g). } { intro f; simpl. apply (invweq (underlyingIso_injectivity _ _)); simpl. apply (invweq (pr1weq_injectivity _ _)). apply funextsec; intro g. simpl. exact ((! (pr2 f) g (unel G)) @ (maponpaths (pr1 f) (runax G g))). } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets. Import UniMath.MoreFoundations.PartA.