proposition: Lemma torsorMapIsIso {G} {X Y : Torsor G} (f : ActionMap X Y) : isweq f.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Combinatorics.OrderedSets