Definition ActionStructure : Type := ∑ (act_mult : action_op G X) (act_unit : ∏ x, act_mult (unel G) x = x), ∏ g h x, act_mult (op g h) x = act_mult g (act_mult h x).
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.