proposition: Lemma torsor_univalence_id {G:gr} (X:Torsor G) : invmap torsor_univalence (idActionIso X) = idpath X.
proof: Proof. change (idActionIso X) with (torsor_univalence (idpath X)). apply homotinvweqweq. 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