From 48222892fbaefc0a516c05c87f4a1bfd46ea799c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:05:07 +0100
Subject: Fix 82--88.

---
 sec/systemt.ltx | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index b534040..309de0f 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -66,12 +66,12 @@ of natural numbers.
 Types in System~T are usually presented as binary trees, with branches
 representing arrows and leaves being \(\nat\). An alternative
 presentation is \emph{argument
-form}~\cite{DBLP:books/sp/LongleyN15}. Notice that all types can be
-written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some unique list of
-argument types \(A_i\). We can therefore represent a type by its list
-of arguments. For example, the type \(\nat\) has argument form \(\epsilon\)
-(the empty list), and the type \(\nat \to \nat \to (\nat \to \nat) \to \nat\)
-has argument form \([\epsilon, \epsilon, [\epsilon]]\).
+form}~\cites{dialectica?}{DBLP:books/sp/LongleyN15}. Notice that all
+types can be written in the form \(A_1 \to \cdots \to A_n \to \nat\) for some
+unique list of argument types \(A_i\). We can therefore represent a
+type by its list of arguments. For example, the type \(\nat\) has
+argument form \(\epsilon\) (the empty list), and the type \(\nat \to \nat \to
+(\nat \to \nat) \to \nat\) has argument form \([\epsilon, \epsilon, [\epsilon]]\).
 
 All System~T types are inhabited.\@ \nat{} is inhabited by zero, and
 any function type is inhabited when its codomain is inhabited by
-- 
cgit v1.2.3

