Merge pull request #163 from williamdemeo/TYPES2021

minor mods

src/Demos/HSP.lagda

@@ -22,7 +22,7 @@ best of our knowledge, it is the first formulation of the HSP theorem in Martin-
 dependent type theory, and the first formal, machine-verified proof of Birkhoff's
 celebrated 1935 result.
 
-In this paper, we present a nearly self-contained formal proof of Birkhoff's theorem by
+In this paper, we present a self-contained formal proof of Birkhoff's theorem by
 extracting into a single Agda module only those parts of the \agdaalgebras library that we
 need for the proof.  The main body of the paper is generated by a literate Agda file which
 is available online\footnote{See
@@ -217,7 +217,7 @@ library are fully constructive and confined to pure Martin-Löf dependent type t
 %In particular, there are no appeals to function extensionality in the present work.
 We are confident that the current version of the \agdaalgebras library\footnote{[REFERENCE
 WITH VERSION INFORMATION NEEDED]} is fully constructive and free from any hidden
-assumptions or inconsistencies that might be used to fool a type-checker.
+assumptions or inconsistencies that could be used to fool a type-checker.
 
 
 %% -----------------------------------------------------------------------------