Use inclusive language in §1.11

Change "his or her" -> "their"

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}%