Definition torsor_mult_weq' {G} (X:Torsor G) (g:G) : X ≃ X. Proof. exists (left_mult g). use isweq_iso. - exact (left_mult (grinv G g)). - intros x. unfold left_mult. intermediate_path ((grinv G g * g)%multmonoid * x). + apply pathsinv0,act_assoc. + intermediate_path (unel G * x). * apply (maponpaths (right_mult x)). apply grlinvax. * apply act_unit. - intros x. unfold left_mult. intermediate_path ((g * grinv G g)%multmonoid * x). + apply pathsinv0,act_assoc. + intermediate_path (unel G * x). * apply (maponpaths (right_mult x)). apply grrinvax. * apply act_unit. 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.