Lemma torsorMapIsIso {G} {X Y : Torsor G} (f : ActionMap X Y) : isweq f. Proof. apply (squash_to_prop (torsor_nonempty X)). - apply isapropisweq. - intros x. set (y := f x). set (f' := λ y', y' / y * x). apply (isweq_iso f f'). + intros x'. unfold f', y. assert (p := quotient_times x' x). refine (_ @ p); clear p. apply (maponpaths (λ g, g * x)). apply quotient_map. + intros y'. unfold f'. assert (p := equivariance f (y'/y) x). refine (p @ _); clear p. fold y. apply quotient_times. 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.