From 9a4522c39e203f3403c1828be103dde6b746f846 Mon Sep 17 00:00:00 2001 From: ThePuzzlemaker Date: Thu, 10 Mar 2022 21:04:37 -0600 Subject: [PATCH] =?UTF-8?q?Use=20inclusive=20language=20in=20=C2=A71.11?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Change "his or her" -> "their" --- preliminaries.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/preliminaries.tex b/preliminaries.tex index 9f37efce0..10c81b2e2 100644 --- a/preliminaries.tex +++ b/preliminaries.tex @@ -1360,7 +1360,7 @@ \section{Propositions as types} \end{equation} so we should be able to translate the above proof into an element of this type. -As an example of how such a translation works, let us describe how a mathematician reading the above English proof might simultaneously construct, in his or her head, an element of~\eqref{eq:tautology2}. +As an example of how such a translation works, let us describe how a mathematician reading the above English proof might simultaneously construct, in their head, an element of~\eqref{eq:tautology2}. The introductory phrase ``Suppose not $A$ and not $B$'' translates into defining a function, with an implicit application of the recursion principle for the cartesian product in its domain $(A\to\emptyt)\times (B\to\emptyt)$. This introduces unnamed variables \index{variable}%