Definition composeActionIso {G:gr} {X Y Z:Action G} (e:ActionIso X Y) (f:ActionIso Y Z) : ActionIso X Z. Proof. revert e f; intros [e i] [f j]. exists (weqcomp e f). destruct e as [e e'], f as [f f']; simpl. apply is_equivariant_comp. exact i. exact j. 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.