fact: 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).
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Combinatorics.OrderedSets