Lemma underlyingIso_incl {G:gr} {X Y:Action G} : isincl (underlyingIso : ActionIso X Y → X ≃ Y). Proof. intros. apply isinclpr1; intro f. apply propproperty. 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.