Definition trivialTorsor_weq (G:gr) (g:G) : (trivialTorsor G) ≃ (trivialTorsor G). Proof. intros. exists (λ h, op h g). apply (isweq_iso _ (λ h, op h (grinv G g))). { exact (λ h, assocax _ _ _ _ @ maponpaths (op _) (grrinvax _ _) @ runax _ _). } { exact (λ h, assocax _ _ _ _ @ maponpaths (op _) (grlinvax _ _) @ runax _ _). } 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.