Definition is_equivariant_comp {G:gr} {X Y Z:Action G} (p:X->Y) (i:is_equivariant p) (q:Y->Z) (j:is_equivariant q) : is_equivariant (funcomp p q). Proof. intros. intros g x. exact (maponpaths q (i g x) @ j g (p x)). 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.