\begin{struct}\label{pointed_set}
    A pointed set $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\pick$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{pointed_refl} $X = X$.
    \end{enumerate}
\end{struct}

\begin{proposition}\label{pointed_carrier}
    Let $X$ be a pointed set.
    Let $x \in X$.
    Then $x \in \carrier[X]$.
\end{proposition}
\begin{proof}
    Follows by assumption.
\end{proof}

\begin{proposition}\label{pointed_operation}
    Let $X$ be a pointed set.
    Then $\pick = \pick[X]$.
\end{proposition}
\begin{proof}
    Follows by assumption.
\end{proof}