proposition: Lemma quotient_map {G} {X Y:Torsor G} (f : ActionMap X Y) (x x':X) : f x' / f x = x' / x.
proof: Proof. refine (! (quotient_uniqueness (f x') (f x) (x' / x) _)). assert (p := equivariance f (x'/x) x). refine (!p @ _); clear p. apply maponpaths. apply quotient_times. Qed.
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