fix the paragraph on setoid, and remove the 'ever'.

src/Demos/HSP.lagda

@@ -7,7 +7,7 @@ logic.
 
 The first major milestone of the \agdaalgebras project is a proof of \emph{Birkhoff's
 variety theorem} (also known as the \emph{HSP theorem})~\cite{Birkhoff:1935}.
-To the best of our knowledge, this constitutes the first ever formal proof of
+To the best of our knowledge, this constitutes the first formal proof of
 Birkhoff's in Martin-Löf Type Theory, and it is the first such machine-verified proof of Birkhoff's
 celebrated 1935 result.  An alternative formalization, based on classical
 set-theory, was achieved in~\cite{birkhoff-in-mizar:1999}; see \href{http://www.mizar.org/JFM/Vol9/birkhoff.html\#BIB21}{mizar.org/JFM/Vol9/birkhoff.html}.
@@ -174,22 +174,17 @@ module _ {A : Type α }{B : A → Type β} where
 A \defn{setoid} is a pair consisting of a type \ab A and
 an equivalence relation \af{≈} on \ab A.  Setoids are useful for representing a
 set with a ``local'' notion of equivalence, instead of always relying on
-the global one as is usually done in set theory. Formal proofs based on setoids
-may seem like an unnatural departure from informal mathematical practice, where
-notions of equality are left implicit and do not distract from what may seem
-like more important, higher-level aspects of the mathematics. However, in our
-view, notions of equality ought to be elevated to a status that obliges us to
-make them explicit in any mathematical argument.  While we acknowledge that formal
-proofs based on setoids may sometimes seem complicated or overly technical, we
-believe that informal arguments, which elide such formalisms, are
-oversimplifications.  We believe it is a bug, not a feature, of informal
-mathematics that proofs need not be explicit about the meaning of equality.
+the global one as is usually done in set theory. In reality, informal
+mathematial practice uses equivalence relations quite pervasively, and
+takes great care to only define equivalence-preserving functions, while
+eliding the actual details. To be fully formal, such details must be given.
+While there are many different approaches for doing that, the one that requires
+no additional meta-theory is based on setoids, which is why we adopt it here.
+While in some settings this has been found by others to be burdensome, we have not
+found it to be so for universal algebra.
 
 \ddmmyydate
 
-\wjd{I tried to make a case for Setoids; JC, can you make this more convincing, or
-  propose something else entirely.}
-
 The \agdaalgebras library was first developed without setoids, relying on
 propositional equality \ad{\au{}≡\au{}} instead,
 along with some experimental, domain-specific types for equivalence classes, quotients, etc.
@@ -2039,7 +2034,7 @@ Let \ab{𝒦} be an arbitrary variety.  We will describe a set of equations that
 % Let \ab{𝒦⁺} := \af{Mod} (\af{Th} \ab{𝒦}). Clearly, \ab{𝒦} \aof{⊆} \ab{𝒦⁺}.  We prove the
 for this choice, we must prove \ab{𝒦} \aof{=} \af{Mod} (\af{Th} \ab{𝒦}).
 Clearly, \ab{𝒦} \aof{⊆} \af{Mod} (\af{Th} \ab{𝒦}).  We prove the
-converse inclusion. Let \ab{𝑨} \af{∈} \af{Mod} (\af{Th} \ab{𝒦}); 
+converse inclusion. Let \ab{𝑨} \af{∈} \af{Mod} (\af{Th} \ab{𝒦});
 it suffices to find an algebra \ab{𝑭} \af{∈} \af{S} (\af{P} \ab{𝒦}) such that
 \ab{𝑨} is a homomorphic image of \ab{𝑭}, as this will show that \ab{𝑨} \af{∈}
 \af{H} (\af{S} (\af{P} \ab{𝒦})) = \ab{𝒦}.
@@ -2166,7 +2161,7 @@ From \ref{item:1} and \ref{item:2} will follow \af{Mod} (\af{Th} (V 𝒦))
 ⊆ \af{H} (\af{S} (\af{P} \ab{𝒦})) (= \af{V} \ab{𝒦}), as desired.
 
 \begin{itemize}
-\item 
+\item
 \noindent \ref{item:1.1}. To define \ab{𝑪} as the product of all algebras in \af{S} \ab{𝒦}, we must first contrive
 an index type for the class \af{S} \ab{𝒦}.  We do so by letting the indices be the algebras
 belonging to \ab{𝒦}. Actually, each index will consist of a triple (\ab{𝑨} , \ab p ,
@@ -2323,7 +2318,7 @@ the proof of \af{F≤C} merely extracts a subalgebra witness from a monomorphism
 
 \end{code}
 Recall, from \ref{item:1.1} and \ref{item:1.2}, we have \ab{𝑪} \af{∈}
-\af{P} (\af{S} \ab{𝒦}) \af{⊆} \af{S} (\af{P} \ab{𝒦}). We now use this, along with 
+\af{P} (\af{S} \ab{𝒦}) \af{⊆} \af{S} (\af{P} \ab{𝒦}). We now use this, along with
 what we just proved (\af{F≤C}), to conclude that \Free{X} belongs to \af{S}
 (\af{P} \ab{𝒦}).
 \begin{code}
@@ -2340,7 +2335,7 @@ This completes stage \ref{item:1} of the proof.
 \end{itemize}
 
 \begin{itemize}
-\item 
+\item
 \noindent \ref{item:2}. We show that every algebra in \af{Mod} (\af{Th} (\af{V}
 \ab{𝒦})) is a homomorphic image of \af{𝔽[~\ab{X}~]}, as follows.
 \ifshort\else
@@ -2368,7 +2363,7 @@ module _ {𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)} where
 \end{code}
 \af{ModTh-closure} and \af{Var⇒EqCl} show that
 \af{V} \ab{𝒦} = \af{Mod} (\af{Th} (\af{V} \ab{𝒦})) holds for every class \ab{𝒦} of \ab{𝑆}-algebras.
-Thus, every variety is an equational class. 
+Thus, every variety is an equational class.
 \end{itemize}
 
 This completes the formal proof of Birkhoff's variety theorem.