Explain the operators and equations on unions.

1 files changed, 6 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index c7506db..cd749a9 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -367,9 +367,14 @@ encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\), of
 a tag indicating which case we are in, and a union which can contain
 a value from any case.
 
+Unions have two operators: \(\mathsf{inj}~i~t\) and
+\(\mathsf{prj}~t~i\) for injecting and projecting values at type
+\(A_i\) respectively. When the two types have the same index, unions
+have the beta reduction rule \(\mathsf{prj}~(\mathsf{inj}~i~t)~i =
+t\). If the two type indices are different then projection is stuck.
+
 \TODO{
   \begin{itemize}
-    \item explain the operations and equations of unions
     \item justify why sums are tagged unions
     \item justify adding union types
     \item justify the case operator on naturals