proposition: Lemma isaset_ActionStructure (G:gr) (X:hSet) : isaset (ActionStructure G X).
proof: Proof. intros. apply isaset_total2. { apply (impred 2); intro g. apply impred; intro x. apply setproperty. } intro op. apply isaset_total2. { apply (impred 2); intro x. apply hlevelntosn. apply setproperty. } intro un. apply (impred 2); intro g. apply (impred 2); intro h. apply (impred 2); intro x. apply hlevelntosn. apply setproperty. Qed.
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