From 5c954d7726e2a2c40b2d426247334ec5ebb678e3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 7 May 2025 15:09:15 +0100
Subject: Fix list append.

---
 sec/encoding.ltx | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'sec/encoding.ltx')

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

