proposition: Lemma free_monoid_theory_algebra_to_setwithbinop_op_is_assoc (A : algebra free_monoid_theory) : isassoc (op (X := free_monoid_theory_algebra_to_setwithbinop A)).
proof: Proof. intros a b c. pose (f := weqvecfun _ [(a ; b ; c)]). pose (Hf := λ i Hi, !(pr_action _ (make_stn 3 i Hi) f)). cbn -[weqvecfun action]. rewrite (Hf 0 (idpath true) : a = _), (Hf 1 (idpath true) : b = _), (Hf 2 (idpath true) : c = _). now do 4 rewrite (move_action_through_weqvecfun f), <- comp_action. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.BinaryOperations UniMath.Algebra.Free_Monoids_and_Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Categories.Monoid UniMath.Combinatorics.Lists UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraCategoryCore UniMath.AlgebraicTheories.AlgebraCategory UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.Examples.FreeObjectTheory