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