test/phase5/exact-contextual-abbreviation-ambiguous.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

\import{test/phase5/exact-contextual-abbreviation.tex}

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

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