8 files changed, 151 insertions, 0 deletions
diff --git a/test/phase5/exact-contextual-abbreviation-ambiguous.tex b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
new file mode 100644
index 0000000..c8fd94c
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-ambiguous.tex
@@ -0,0 +1,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}
diff --git a/test/phase5/exact-contextual-abbreviation-consumer.tex b/test/phase5/exact-contextual-abbreviation-consumer.tex
new file mode 100644
index 0000000..f2e1ceb
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-consumer.tex
@@ -0,0 +1,11 @@
+\import{test/phase5/exact-contextual-abbreviation.tex}
+
+\begin{abbreviation}\label{phase5_context_quantified}
+    $a$ is phase five universally absorbing iff
+    for all $b$ we have $a\phasefivedot b = a$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{phase5_context_quantified_explicit}
+    $A$ is a phase five explicit universal absorber of $a$ iff
+    for all $b$ we have $\phasefivecombine[A](a,b) = a$.
+\end{abbreviation}
diff --git a/test/phase5/exact-contextual-abbreviation-missing.tex b/test/phase5/exact-contextual-abbreviation-missing.tex
new file mode 100644
index 0000000..cecbbf2
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation-missing.tex
@@ -0,0 +1,6 @@
+\import{test/phase5/exact-contextual-abbreviation.tex}
+
+\begin{proposition}\label{phase5_context_missing}
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = b\phasefivedot a$.
+\end{proposition}
diff --git a/test/phase5/exact-contextual-abbreviation.tex b/test/phase5/exact-contextual-abbreviation.tex
new file mode 100644
index 0000000..9b4387e
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation.tex
@@ -0,0 +1,56 @@
+\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}
diff --git a/test/phase5/exact-local-function-failure.tex b/test/phase5/exact-local-function-failure.tex
new file mode 100644
index 0000000..f1afc9b
--- /dev/null
+++ b/test/phase5/exact-local-function-failure.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{phase5_local_function_failure}
+    For all $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $f(x) = f$ for $x\in A$.
+    Follows by assumption.
+\end{proof}
diff --git a/test/phase5/exact-local-function.tex b/test/phase5/exact-local-function.tex
new file mode 100644
index 0000000..03e6ce4
--- /dev/null
+++ b/test/phase5/exact-local-function.tex
@@ -0,0 +1,18 @@
+\begin{signature}\label{phase5_local_pair}
+    $(x,y)$ is a set.
+\end{signature}
+
+\begin{proposition}\label{phase5_local_function}
+    For all $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $f(x) = x$ for $x\in A$.
+    Show for all $y$ we have if $y\in A$, then $(y,y)\in f$.
+    \begin{subproof}
+        Fix $y$.
+        Assume $y\in A$.
+        Follows by assumption.
+    \end{subproof}
+    Follows by assumption.
+\end{proof}
diff --git a/test/phase5/exact-structure-child.tex b/test/phase5/exact-structure-child.tex
new file mode 100644
index 0000000..b9f1e36
--- /dev/null
+++ b/test/phase5/exact-structure-child.tex
@@ -0,0 +1,8 @@
+\import{test/phase5/exact-structure.tex}
+
+\begin{struct}\label{marked_pointed_set}
+    A marked pointed set $X$ is a pointed set such that
+    \begin{enumerate}
+        \item\label{marked_pointed_refl} $\pick[X] = \pick$.
+    \end{enumerate}
+\end{struct}
diff --git a/test/phase5/exact-structure.tex b/test/phase5/exact-structure.tex
new file mode 100644
index 0000000..b1a0d86
--- /dev/null
+++ b/test/phase5/exact-structure.tex
@@ -0,0 +1,27 @@
+\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}