Lemma isaset_ActionStructure (G:gr) (X:hSet) : isaset (ActionStructure G X). 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.
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.