summaryrefslogtreecommitdiff
path: root/sec/encoding.ltx
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-05-07 15:09:15 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-05-07 15:09:15 +0100
commit5c954d7726e2a2c40b2d426247334ec5ebb678e3 (patch)
tree34a0f0fdf9727a19547af71b23601655dabc7da3 /sec/encoding.ltx
parent468852215a59d502dc156346df97f2d2f902203b (diff)
Fix list append.
Diffstat (limited to 'sec/encoding.ltx')
-rw-r--r--sec/encoding.ltx9
1 files changed, 5 insertions, 4 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index b697150..b93ca8f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -491,10 +491,11 @@ At this point, the only type former not present in System~T is the
union type.\@ \textcite{oleg} gives an inductive encoding for binary
unions. We instead use an encoding for unions derived from the
argument form of types. Given we have a family of types \(A_i\) in
-argument form, their union is the concatenation \(A_1 ++ A_2 ++ \cdots ++
-A_n\). To inject type \(A_k\) into the union, we ignore the function
-arguments for all the other type constructors. To project type \(A_k\)
-out of the union, we pass \(\mathsf{arb}\) to all the other arguments.
+argument form, their union is the concatenation \(A_1 \append A_2
+\append \cdots \append A_n\). To inject type \(A_k\) into the union, we
+ignore the function arguments for all the other type constructors. To
+project type \(A_k\) out of the union, we pass \(\mathsf{arb}\) to all
+the other arguments.
Using this argument-form union, we remove the need to perform
induction on types, and only have to iterate over the number of types