From 27d17d272cb291ca3838565bb0f1c2dfbe630983 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 May 2025 15:43:50 +0100
Subject: Explain the operators and equations on unions.

---
 sec/encoding.ltx | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3