Definition torsor_univalence_transport {G:gr} {X Y:Torsor G} (p:X=Y) (x:X) : torsor_univalence p x = transportf (λ X:Torsor G, X:Type) p x. Proof. now induction p. 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.