delete trailing whitespace

EuclideanGeometry.tex

@@ -69,7 +69,7 @@ \section{Inner product spaces}
 action with the projection map $\B \OrthGp n \to \typeRealVectorSpace$ that
 forgets the inner product to get an action of $\OrthGp n$ on the vector space
 $\RR^n$.
-  
+
 \section{Euclidean spaces}
 
 \begin{definition}\label{def:EuclideanSpace}

book.tex

@@ -39,7 +39,7 @@ \section{ruler and compass constructions}
 \section{affine planes and Pappus' law}
 \section{projective planes}
 \chapter{Vector spaces and linear groups}
-Quotients; subspaces (= ?). Bases and so. Dual space; orthogonality. (all of this depends on good implementations of subobjects). Eigen-stuff. Characteristic polynomials; Hamilton-Cayley. 
+Quotients; subspaces (= ?). Bases and so. Dual space; orthogonality. (all of this depends on good implementations of subobjects). Eigen-stuff. Characteristic polynomials; Hamilton-Cayley.
 \section{the algebraic hierarchy: groups, abelian groups, rings, fields}
 \section{vector spaces}
 \section{the general linear group as automorphism group}

intro.tex

@@ -122,15 +122,15 @@ \section*{Glossary of coercions}
 \item If $p: A= B$ with $A$ and $B$ types, then we use $\ptoe p$ for the canonical
 equivalence from $A$ to $B$ (also only as function).
 %\item If $G$ is the group $(A,a,p,q)$, then $g:G$ means $g: a=_A a$. %TODO: El
-\item If $X$ is $(A,a,\ldots)$ with $a:A$, then $\pt_X$ and even just $\pt$ mean $a$. 
+\item If $X$ is $(A,a,\ldots)$ with $a:A$, then $\pt_X$ and even just $\pt$ mean $a$.
 \end{itemize}
 
 \bigskip
 
 \section*{Acknowledgement.}
 The authors acknowledge the support of the Centre for Advanced Study (CAS)
 at the Norwegian Academy of Science and Letters
-in Oslo, Norway, which funded and hosted the research project Homotopy  
+in Oslo, Norway, which funded and hosted the research project Homotopy
 Type Theory and Univalent Foundations during the academic year 2018/19.
 
 

macros.tex

@@ -553,17 +553,17 @@
 \newcommand*{\Gtorsor}{\Tors_G}
 \newcommand*{\Xtorsor}[1]{\Tors_{#1}}%      added by MAB
 \newcommand*{\Ztorsor}{\Xtorsor{\zet}}
-\newcommand*{\TorZ}{{\constant{T}\ZZ}} % {\mathbf{TorZor}}% alternative: BZ.   
+\newcommand*{\TorZ}{{\constant{T}\ZZ}} % {\mathbf{TorZor}}% alternative: BZ.
 \newcommand*{\SetBundle}{\constant{SetBundle}}             % end MAB
 \newcommand*{\typegroup}{\Group}
 \newcommand*{\typeabgroup}{\AbGroup}
-\newcommand*{\typesubgroup}{\constant{Sub}}%"gp" removed - is evident from the type of the subscript G           
+\newcommand*{\typesubgroup}{\constant{Sub}}%"gp" removed - is evident from the type of the subscript G
 \newcommand*{\typemono}{\constant{Mono}}%monomorphisms into a group (subscript)
 \newcommand*{\typeepi}{\constant{Epi}}%epimorphisms out of a group (subscript)
 \newcommand*{\typenormal}{\constant{Nor}}
 \newcommand*{\typeset}{\Set}
 \newcommand*{\typeinftygp}{{\infty}\Group}
-\newcommand*{\typemonoid}{\Monoid} 
+\newcommand*{\typemonoid}{\Monoid}
 \newcommand*{\typetorsor}{\Tors}
 \newcommand*{\pttype}{\UUp}
 \newcommand*{\typeabsgp}{\Group_{\textup{Abstract}}}
@@ -634,7 +634,7 @@
 \newcommand{\coqdocbasebaseurl}{https://unimath.github.io/doc/UniMath/\shorthash/}
 
 %\coqident call are relative to this long path
-\newcommand{\coqdocbaseurl}{\coqdocbasebaseurl UniMath.} 
+\newcommand{\coqdocbaseurl}{\coqdocbasebaseurl UniMath.}
 \newcommand{\urlhash}{\#}
 
 \newcommand{\coqdocurl}[2]{\coqdocbaseurl #1.html\urlhash #2}
@@ -644,7 +644,7 @@
 \makeatletter
 \newcommand{\coqident}{\begingroup\@makeother\#\@coqident}
 \newcommand{\@coqident}[3][]{% empty default first and optional argument
-  \ifthenelse{\isempty{#2}}% 
+  \ifthenelse{\isempty{#2}}%
   {\nolinkcoqident{#3}}%           [optional]{}{printme}
   {\ifthenelse{\isempty{#1}}%
   {\href{\coqdocurl{#2}{#3}}{\nolinkcoqident{#3}}}% []{file}{identifier+printed}
@@ -654,7 +654,7 @@
 \newcommand{\coqfile}[2]{%
   \ifthenelse{\isempty{#1}}%
   {\href{\coqdocbaseurl #2.html}{#2.v}}%
-  {\href{\coqdocbaseurl #1.#2.html}{#2.v}}} 
+  {\href{\coqdocbaseurl #1.#2.html}{#2.v}}}
 \makeatother
 
 %sususe is a replacement for subsubsection.  sususe is the same as subsubsection but numbers correctly bid

papers.bib

@@ -28,7 +28,7 @@ @Misc{UniMath
     title = {{UniMath --- a computer-checked library of univalent mathematics}},
     howpublished = {{available} at \url{http://UniMath.org}}
  }
-                  
+
 @Misc{Lean,
  title = {Lean theorem prover},
  howpublished = {a proof assistant together with a library of formalized proofs, available at \url{https://github.com/leanprover/lean}}}
@@ -42,7 +42,7 @@ @Misc{HoTT
           title = {{The HoTT Library}},
           howpublished = {a Coq library of formalized proofs, available at \url{https://github.com/HoTT/HoTT}}
         }
-                  
+
 @Misc{HoTT-Agda,
           title = {{Homotopy Type Theory in Agda}},
           howpublished = {an Agda library of formalized proofs, available at \url{https://github.com/HoTT/HoTT-Agda}}
@@ -99,7 +99,7 @@ @incollection {MR0387009
   MRNUMBER = {0387009 (52 \#7856)},
 MRREVIEWER = {Horst Luckhardt},
 }
-                  
+
 @incollection {39,
     AUTHOR = {Voevodsky, Vladimir},
      TITLE = {Subsystems and regular quotients of {C}-systems},
@@ -208,7 +208,7 @@ @article {MR3607210
 MRREVIEWER = {Thomas Streicher},
 }
 
-	
+
 
 @article {MR3607209,
     AUTHOR = {Voevodsky, Vladimir},
@@ -222,7 +222,7 @@ @article {MR3607209
    MRCLASS = {18D15 (03F50)},
   MRNUMBER = {3607209},
 }
-	
+
 
 @Misc{1211.2851,
     Author = {Kapulkin, Chris and Lumsdaine, Peter LeFanu},
@@ -260,7 +260,7 @@ @Book{constructive-algebra
   publisher = {Springer-Verlag},
   note =   {Relevant Exercise 5 on page 133},
   year =      1988}
-                  
+
 @article {AwodeyBauer_prop_as_types,
     AUTHOR = {Awodey, Steven and Bauer, Andrej},
      TITLE = {Propositions as [types]},
@@ -310,7 +310,7 @@ @incollection {MR1678360
        DOI = {10.1007/978-3-662-22108-2_11},
        URL = {http://dx.doi.org/10.1007/978-3-662-22108-2_11},
 }
-                  
+
 @article {MR2463991,
     AUTHOR = {Gonthier, Georges},
      TITLE = {Formal proof---the four-color theorem},
@@ -356,7 +356,7 @@ @article {bernays-7
   MRNUMBER = {0066320},
 MRREVIEWER = {O. Frink},
 }
-		
+
 @article {bernays-6,
     AUTHOR = {Bernays, Paul},
      TITLE = {A system of axiomatic set theory. {VI}},
@@ -372,7 +372,7 @@ @article {bernays-6
        DOI = {10.2307/2267328},
        URL = {http://dx.doi.org/10.2307/2267328},
 }
-		
+
 @article {bernays-5,
     AUTHOR = {Bernays, Paul},
      TITLE = {A system of axiomatic set theory. {V}. {G}eneral set theory},
@@ -388,7 +388,7 @@ @article {bernays-5
        DOI = {10.2307/2271051},
        URL = {http://dx.doi.org/10.2307/2271051},
 }
-		
+
 @article {bernays-4,
     AUTHOR = {Bernays, Paul},
      TITLE = {A system of axiomatic set theory},
@@ -404,7 +404,7 @@ @article {bernays-4
        DOI = {10.2307/2268110},
        URL = {http://dx.doi.org/10.2307/2268110},
 }
-		
+
 @article {bernays-3,
     AUTHOR = {Bernays, Paul},
      TITLE = {A system of axiomatic set theory. {III}. {I}nfinity and
@@ -421,7 +421,7 @@ @article {bernays-3
        DOI = {10.2307/2266303},
        URL = {http://dx.doi.org/10.2307/2266303},
 }
-		
+
 @article {bernays-2,
     AUTHOR = {Bernays, Paul},
      TITLE = {A system of axiomatic set theory. {P}art {II}},
@@ -461,7 +461,7 @@ @Misc{1610.04591
     Year = {2016},
     note = {\arxiv{1610.04591}},
 }
-                  
+
 @article {IMGelfand,
     AUTHOR = {Beilinson, A.},
      TITLE = {I. {M}. {G}elfand and his seminar---a presence},
@@ -477,7 +477,7 @@ @article {IMGelfand
   MRNUMBER = {3445168},
        URL = {https://doi-org.proxy2.library.illinois.edu/10.1090/noti1337},
 }
-                  
+
 @Misc{1605.03227,
     Author = {Hou, Kuen-Bang Hou (Favonia) and Finster, Eric and Licata, Dan and Lumsdaine, Peter LeFanu},
     Title = {{A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory}},
@@ -590,7 +590,7 @@ @Article{	  Shulman-Real-Cohesive
   year		= {2018},
   pages		= {856–941}
 }
-                  
+
 @incollection {MR0274219,
     AUTHOR = {de Bruijn, N. G.},
      TITLE = {The mathematical language {AUTOMATH}, its usage, and some of
@@ -663,7 +663,7 @@ @incollection {MR3323808
   MRNUMBER = {3323808},
 MRREVIEWER = {Thomas John Hunter},
 }
-	
+
 @incollection {MR3281415,
     AUTHOR = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
      TITLE = {A model of type theory in cubical sets},
@@ -782,7 +782,7 @@ @article {MR0543793
 MRREVIEWER = {Frank Allaire},
        URL = {http://projecteuclid.org/euclid.ijm/1256049012},
 }
-		
+
 @article {MR0543792,
     AUTHOR = {Appel, K. and Haken, W.},
      TITLE = {Every planar map is four colorable. {I}. {D}ischarging},
@@ -798,7 +798,7 @@ @article {MR0543792
 MRREVIEWER = {Frank Allaire},
        URL = {http://projecteuclid.org/euclid.ijm/1256049011},
 }
-		
+
 @InProceedings{10.1007/978-3-642-39634-2_14,
 author="Gonthier, Georges
 and Asperti, Andrea
@@ -857,7 +857,7 @@ @Misc{1802.01170
 @Misc{1802.02191,
  title = {{Cellular Cohomology in Homotopy Type Theory}},
  author = {Buchholtz, Ulrik and Hou, Kuen-Bang (Favonia)},
- year = {February, 2018}, 
+ year = {February, 2018},
  note = {\arxiv{1802.02191}}}
 
 @article{Kleiner-group-survey,