proposition: Lemma is_torsor_isaprop {G:gr} (X:Action G) : isaprop (is_torsor X).
proof: Proof. intros. apply isapropdirprod. { apply propproperty. } { apply impred; intro x. apply isapropisweq. } 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