\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Data.List
\import Function
\import Paths.Meta

\func universalFreeMonoidMap {S : \Set} {M : Monoid} (in : S -> M) : MonoidHom (ListMonoid {S}) M \cowith
  | func => extension
  | func-ide => idp
  | func-* => helper
  \where {
    \func extension (list : ListMonoid {S}) : M \elim  list
      | nil => M.ide
      | a :: l => in a * extension l

    \func helper  {x y : List S}
      : extension (x ++ y) = extension x M.* extension  y \elim x {
      | nil => rewrite M.ide-left idp
      | _ :: l => rewrite (M.*-assoc, helper {_} {_} {_} {l}) idp
  }
}

\func isMonoidGenerated {M : Monoid} {S : \Set} (j : S -> M)
  => IsSurj (universalFreeMonoidMap j)