\import{algebra/semigroup.tex}
\section{Monoid}\label{form_sec_monoid}

\begin{struct}\label{monoid}
    A monoid $A$ is a unital magma such that
    \begin{enumerate}
        \item\label{monoid_assoc} for all $a,b,c\in\carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$.
    \end{enumerate}
\end{struct}

\begin{corollary}\label{monoid_implies_semigroup}
    Let $A$ be a monoid. Then $A$ is a semigroup.
\end{corollary}
\begin{proof}
    Follows by \cref{monoid,unitalmagma,semigroup}.
\end{proof}
