Definition iterop_unoseq_mon {M:abmonoid} : MultipleOperation M. Proof. intros m. induction m as [J m]. induction J as [I fin]. simpl in m. unfold isfinite, finstruct in fin. simple refine (squash_to_set (setproperty M) (λ (g : finstruct I), iterop_fun_mon (m ∘ g : _ → M)) _ fin). intros. induction x as [n x]. induction x' as [n' x']. assert (p := weqtoeqstn (invweq x' ∘ x)%weq). induction p. assert (w := commutativityOfProducts (m ∘ x') (invweq x' ∘ x)%weq). simple refine (_ @ ! w); clear w. unfold iterop_seq_mon, iterop_fun_mon, iterop_seq. apply maponpaths. rewrite weqcomp_to_funcomp. apply funextfun; intro i. simpl. apply maponpaths. exact (! homotweqinvweq x' (x i)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.