From 2f3b9a6afffa0f2345a3543566c95753770d5238 Mon Sep 17 00:00:00 2001
From: Fangyi Zhou <me@fangyi.io>
Date: Mon, 6 May 2019 16:03:15 +0100
Subject: [PATCH] =?UTF-8?q?Connectives:=20Use=20unicode=20=C3=97=20instead?=
 =?UTF-8?q?=20of=20x?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/plfa/Connectives.lagda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index 5b8ea415..8b36ad5f 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -136,7 +136,7 @@ infixr 2 _×_
 \end{code}
 Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
 
-Given two types `A` and `B`, we refer to `A x B` as the
+Given two types `A` and `B`, we refer to `A × B` as the
 _product_ of `A` and `B`.  In set theory, it is also sometimes
 called the _Cartesian product_, and in computing it corresponds
 to a _record_ type. Among other reasons for