proposition: Lemma mor_action_ax_identity (A : algebra free_monoid_theory) (n : nat) (f : free_monoid_theory n) (a : stn n → (monoid_to_algebra (free_monoid_theory_algebra_to_monoid A) : algebra _)) : mor_action_ax (identity _) (idfun A) (@action free_monoid_theory (monoid_to_algebra (free_monoid_theory_algebra_to_monoid A) : algebra _)) (@action free_monoid_theory A) n f a.
proof: Proof. pose (A' := monoid_to_algebra (free_monoid_theory_algebra_to_monoid A) : algebra _). apply (list_ind (λ x, action (A := A') x a = action (A := A) x a)). - exact (!(lift_constant_action (A := A) _ (unel _) a)). - intros i xs Haction. refine (comp_action A' op_el (weqvecfun _ [(free_monoid_unit i ; xs)]) a @ !_). refine (comp_action A op_el (weqvecfun _ [(free_monoid_unit i ; xs)]) a @ !_). now rewrite <- (move_action_through_weqvecfun (A := A) a), <- Haction, (pr_action A _ _ : action (free_monoid_unit i : free_monoid_theory n) _ = _). 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