proposition: Lemma free_monoid_theory_algebra_to_isunit (A : algebra free_monoid_theory) : isunit (op (X := free_monoid_theory_algebra_to_setwithbinop A)) (free_monoid_theory_algebra_to_unit A).
proof: Proof. split; intro x; cbn -[weqvecfun action]; now rewrite <- (pr_action _ (make_stn 1 0 (idpath _)) (λ _, x)), <- (lift_constant_action 1 _ (λ _, x) : _ = free_monoid_theory_algebra_to_unit A), (move_action_through_weqvecfun (λ _, x)), <- 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