Lemma ActionIso_isaset {G:gr} (X Y:Action G) : isaset (ActionIso X Y). Proof. apply (isofhlevelsninclb _ pr1). { apply isinclpr1; intro f. apply propproperty. } apply isofhlevelsnweqtohlevelsn. apply setproperty. 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.