1 files changed, 27 insertions, 0 deletions
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}