diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/encoding.ltx | 7 |
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 |