From 40c6505ae20614a6667cd4b79c69d53a9e45203e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Wed, 22 Dec 2021 16:15:16 +0000
Subject: [PATCH] Simplify

---
 thesis.tex | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/thesis.tex b/thesis.tex
index 71df85f..4d43184 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -6001,20 +6001,20 @@ Kind and type environments are right-extended sequences of bindings. A
 kind environment binds type variables to their kinds, whilst a type
 environment binds term variables to their types.
 
-\paragraph{Type variables} The type structure has three syntactically
-distinct type variables (the kinding system gives us five semantically
-distinct notions of type variables). As we sometimes wish to refer
-collectively to type variables, we define the set of type variables,
-$\TyVarCat$, to be generated by:
-%
-\[
-  \TyVarCat \defas
-  \ba[t]{@{~}l@{~}l}
-         &\{ A \in \ValTypeCat  \mid A \text{ has the form } \alpha \}\\
-    \cup &\{ R \in \RowCat      \mid R \text{ has the form } \rho   \}\\
-    \cup &\{ P \in \PresenceCat \mid P \text{ has the form } \theta \}
-  \ea
-\]
+% \paragraph{Type variables} The type structure has three syntactically
+% distinct type variables (the kinding system gives us five semantically
+% distinct notions of type variables). As we sometimes wish to refer
+% collectively to type variables, we define the set of type variables,
+% $\TyVarCat$, to be generated by:
+% %
+% \[
+%   \TyVarCat \defas
+%   \ba[t]{@{~}l@{~}l}
+%          &\{ A \in \ValTypeCat  \mid A \text{ has the form } \alpha \}\\
+%     \cup &\{ R \in \RowCat      \mid R \text{ has the form } \rho   \}\\
+%     \cup &\{ P \in \PresenceCat \mid P \text{ has the form } \theta \}
+%   \ea
+% \]
 
 % Value types comprise the function type $A \to C$, whose domain
 % is a value type and its codomain is a computation type $B \eff E$,