Definition left_mult_Iso {G:abgr} (X:Torsor G) (g:G) : ActionIso X X. Proof. exists (torsor_mult_weq' X g). intros h x. change (g * (h * x) = h * (g * x)). refine (! ac_assoc X g h x @ _ @ ac_assoc X h g x). exact (maponpaths (right_mult x) (commax G g h)). 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.