Definition is_equivariant_identity {G:gr} {X Y:Action G} (p:ac_set X = ac_set Y) : p # ac_str X = ac_str Y ≃ is_equivariant (cast (maponpaths pr1hSet p)). Proof. revert X Y p; intros [X [Xm [Xu Xa]]] [Y [Ym [Yu Ya]]] ? . simpl in p. destruct p; simpl. unfold transportf; simpl. simple refine (make_weq _ _). { intros p g x. simpl in x. simpl. exact (eqtohomot (eqtohomot (maponpaths act_mult p) g) x). } use isweq_iso. { unfold cast; simpl. intro i. assert (p:Xm=Ym). { apply funextsec; intro g. apply funextsec; intro x; simpl in x. exact (i g x). } destruct p. clear i. assert (p:Xu=Yu). { apply funextsec; intro x; simpl in x. apply setproperty. } destruct p. assert (p:Xa=Ya). { apply funextsec; intro g. apply funextsec; intro h. apply funextsec; intro x. apply setproperty. } destruct p. apply idpath. } { intro p. apply isaset_ActionStructure. } { intro is. apply proofirrelevance. apply impred; intros g. apply impred; intros x. 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.