\begin{signature}\label{phase5_context_apply}
    $\apply{f}{x}$ is a set.
\end{signature}

\begin{signature}\label{phase5_context_pair}
    $(a,b)$ is a set.
\end{signature}

\begin{struct}\label{phase5_context_magma}
    A phase five context magma $A$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\phasefivecombine$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{phase5_context_refl} $A = A$.
    \end{enumerate}
\end{struct}

\begin{struct}\label{phase5_context_unital_magma}
    A phase five context unital magma $A$ is a phase five context magma.
\end{struct}

\begin{abbreviation}\label{phase5_context_dot}
    %! infixl 4
    $a\phasefivedot b = \phasefivecombine(a,b)$.
\end{abbreviation}

\begin{abbreviation}\label{phase5_context_commutes}
    $a$ phase five commutes with $b$ iff
    $a\phasefivedot b = b\phasefivedot a$.
\end{abbreviation}

\begin{proposition}\label{phase5_context_dot_explicit}
    Let $A$ be a phase five context magma.
    Let $a,b$ be sets.
    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
\end{proposition}

\begin{proposition}\label{phase5_context_inherited}
    Let $A$ be a phase five context unital magma.
    Let $a,b$ be sets.
    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
\end{proposition}

\begin{proposition}\label{phase5_context_nested}
    Let $A$ be a phase five context magma.
    Let $a,b$ be sets.
    Then $a$ phase five commutes with $b$ iff
        $\phasefivecombine[A](a,b) = \phasefivecombine[A](b,a)$.
\end{proposition}

\begin{proposition}\label{phase5_context_explicit_unique}
    Let $A,a,b$ be sets.
    Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
\end{proposition}