diff --git a/README.md b/README.md
index bf19ad9..2c88c77 100644
--- a/README.md
+++ b/README.md
@@ -8,9 +8,9 @@ This book will be an undergraduate textbook written in the univalent style, taki
 - An element of a proposition can be called a *proof*.
 - Identity types are denoted in general using the macro \eqto, which produces ⥱ (that is an arrow with an = on top). An element of an identity type is called an *identification*, and otherwise a *path*. We may say that it shows how to *identify* two elements.
   If the type is a set, we may denote its identity types by a = b and call them *equations*. When a = b has an element we say that a and b are *equal*.
-- Types similar to identity types, like the type of eqivalences from A to B, are also denoted with a macro ending in "to", like \equivto, producing ⥲ (that is an arrow with an equivalence sign on top).
+- Types similar to identity types, like the type of equivalences from A to B, are also denoted with a macro ending in "to", like \equivto, producing ⥲ (that is an arrow with an equivalence sign on top).
 - The type containing the variable in a family is called the "parameter type", not the "index type", nor the "base type".
-- Being equal by definiton is denoted with three lines and is called just that, and not *definitionally equal* or *judgmentally equal*.
+- Being equal by definition is denoted with three lines and is called just that, and not *definitionally equal* or *judgmentally equal*.
 - A synonym of "function" is "map".  We don't use "mapping" or "application" as synonyms.
 - In the preliminary chapters (up to subgroups), the underlying set map U from groups to sets has to be applied explicitly. Thereafter, it can be a coercion.
 - Composition of p: a⥱b and q: b⥱c is denoted by either p∗q (p\ct q), or by q·p (q\cdot p), qp or q∘p (q\circ p). The latter is preferred when p and q come from equivalences.
@@ -36,7 +36,7 @@ This book will be an undergraduate textbook written in the univalent style, taki
     10 Κ κ, 11 Λ λ, 12 Μ μ, 13 Ν ν, 14 Ξ ξ, 15 Ο ο, 16 Π π, 17 Ρ ρ, 18 Σ σ, 19 Τ τ,
     20 Υ υ, 21 Φ φ, 22 Χ χ, 23 Ψ ψ, and 24 Ω ω;
     ```
-  + for identifiers in the Roman alphabet use the name (e.g., for $\Ker$ use (Ker) or (ker);
+  + for identifiers in the Roman alphabet use the name (e.g., for $\Ker$ use (Ker) or (ker));
 - Given a: A, we refer to elements of a ⥱ a as either symmetries *of* a, or symmetries *in* A.
 
 ## Current draft of the book
diff --git a/circle.tex b/circle.tex
index a97bc7c..04bd9d5 100644
--- a/circle.tex
+++ b/circle.tex
@@ -627,7 +627,7 @@ \section{\Coverings}
 the other interpretation ``all the preimages are connected''
 would simply give us an equivalence (since connected sets are contractible),
 and this is \emph{not} what is intended. (Equivalences are \coverings,
-but not necessarily connected \coverings and connected \coverings are not neccesarily equivalences.)
+but not necessarily connected \coverings and connected \coverings are not necessarily equivalences.)
 
 Likewise for the other qualifications; for instance, in a ``finite \covering'' $f:A\to B$,
 all fibers are finite sets, but 
@@ -3344,7 +3344,7 @@ \section{Universal property of $\Cyc_n$}
   $\hat p_x(\blank\sigma_n) = \hat p_x(\blank) \sigma$. By setting $p \jdeq \hat
   p_{\pt_n}(\refl {\pt_n})$, we would have succeeded. Indeed, path induction on
   $\alpha: x \eqto x'$ shows that $\hat p_{x'}(\alpha \blank) = \ap f (\alpha) \hat
-  p_x(\blank)$ on one hand, and the hyptohesis on $\hat p$ proves that $\hat
+  p_x(\blank)$ on one hand, and the hypothesis on $\hat p$ proves that $\hat
   p_{\pt_n} (\blank) \sigma = \hat p_{\pt_n}(\blank \sigma_n)$ on the other
   hand. This leads to the chain of equations:
   \begin{align*}
diff --git a/fingp.tex b/fingp.tex
index 5497544..5ce9aa5 100644
--- a/fingp.tex
+++ b/fingp.tex
@@ -44,7 +44,7 @@ \section{Brief overview of the chapter}
 \label{sec:fingp-overview}
 We start by giving the above-mentioned counting version \cref{lem:Lagrangeascounting} of Lagrange's theorem \cref{thm:lagrange}.  
 We then moves on to prove Cauchy's \cref{thm:cauchys} stating that any finite group whose cardinality is divisible by a prime $p$ has a cyclic subgroup of cardinality $p$.
-Cauchchy's theorem has many applications, and we use it already in \cref{sec:sylow} in the proof of Sylow's Theorems which give detailed information about the subgroups of a given finite group $G$.  Sylow's theorems is basically a study of the $G$-set of subgroups of $G$ from a counting perspective.  
+Cauchy's theorem has many applications, and we use it already in \cref{sec:sylow} in the proof of Sylow's Theorems which give detailed information about the subgroups of a given finite group $G$.  Sylow's theorems is basically a study of the $G$-set of subgroups of $G$ from a counting perspective.  
 In particular, if $p^n$ divides the cardinality of $G$, but $p^{n+1}$ does not, then Sylow's Third \cref{thm:sylow3} gives valuable information about the cardinality of the $G$-set of subgroups of $G$ of cardinality $p^n$.
 
 
@@ -137,7 +137,7 @@ \section{Cauchy's theorem}
 % $$A(S,j)\defequi ((S,j)=(S,j)\to \USym G).$$  Since we have an equivalence $j^?:\bn p\to ((S,j)=(S,j))$ we get that $J:A(S,j)\to \prod_{\bn p}\USym G$ given by $J(g)=(g_{j^0},g_{j_1},\dots,g_{j^{p-1}})$ is an equivalence.
 Given a set $A$, a function $a : \bn p \to A$ is an ordered $p$-tuple of elements of $A$: it suffices to write $a_i$ for $a(i)$ to retrieve the
 usual notations for tuples. Given $(S,j) : \B\CG_p$ however, functions $S \to A$ cannot really be thought the same because $S$ is not
-explicitely enumerated. But as soon as we are given $q : \zet/p \eqto (S,j)$, then functions $S \to A$ are just as good to model ordered
+explicitly enumerated. But as soon as we are given $q : \zet/p \eqto (S,j)$, then functions $S \to A$ are just as good to model ordered
 $p$-tuples of $A$ (just by precomposing with the first projection of $q$). With this in mind, define $\mu_p : (\bn p \to \USym G) \to \USym G$
 to be the $p$-ary multiplication, meaning $\mu_p (g) \defequi g_0g_1\ldots g_{p-1}$. Then, one can define
 $\mu:\prod_{(S,j):\B\CG_p}(\zet/p \eqto (S,j)) \to (S\to\USym G)\to \USym G$ by $\mu_{(S,j)}(q)(g)\defequi (gq)_{0}\cdot\dots\cdot (gq)_{p-1}$
diff --git a/galois.tex b/galois.tex
index e46fe6c..c98654d 100644
--- a/galois.tex
+++ b/galois.tex
@@ -4,7 +4,7 @@ \chapter{Galois theory}%
 %% VERY PRELIMINARY
 The goal of Galois theory is to study how the roots of a given polynomial can
 be distinguished from one another. Take for example $X^2+1$ as a polynomial
-with real coefficients. It has two distincts roots in $\mathbb C$, namely $i$
+with real coefficients. It has two distinct roots in $\mathbb C$, namely $i$
 and $-i$. However, an observer, who is limited to the realm of $\mathbb R$,
 can not distinguish between the two. Morally speaking, from the point of view
 of this observer, the two roots $i$ and $-i$ are pretty much the same. Formally
@@ -12,7 +12,7 @@ \chapter{Galois theory}%
 satisfied if and only if $Q(-i,i) = 0$ also. This property is easily understood
 by noticing that there is a automorphism of fields $\sigma: \mathbb C  \to
 \mathbb C$ such that $\sigma(i) = -i$ and $\sigma(-i) = i$ which also fixes
-$\mathbb R$. The goal of this chapter is to provide the rigourous framework in
+$\mathbb R$. The goal of this chapter is to provide the rigorous framework in
 which this statement holds.
 {\color{red} TODO: complete/rewrite the introduction}
 
@@ -143,7 +143,7 @@ \section{Covering spaces and field extensions}
   equivalence. However, the converse is false, as shown by the non-algebraic
   extension $\mathbb Q \hookrightarrow \mathbb R$. We will prove that every
   $\mathbb Q$-endomorphism of $\mathbb R$ is the identity function. Indeed, any
-  $\mathbb Q$-endormorphism $\varphi : \mathbb R \to \mathbb R$ is linear and
+  $\mathbb Q$-endomorphism $\varphi : \mathbb R \to \mathbb R$ is linear and
   sends squares to squares, hence is non-decreasing. Let us now take an irrational
   number $\alpha:\mathbb R$. For any rational $p,q:\mathbb Q$ such that $p <
   \alpha < q$, then $p = \varphi(p) < \varphi(\alpha) < \varphi(q) = q$. Hence
@@ -171,7 +171,7 @@ \section{Intermediate extensions and subgroups}
 characterize those extensions $i':k \to L$ for which all subgroups of
 $\Gal(L,i')$ arise in this way. 
 
-Given any extension $i:k \to L$, there is an obivous $\Gal(L,i)$-set $X$ given by 
+Given any extension $i:k \to L$, there is an obvious $\Gal(L,i)$-set $X$ given by 
 \begin{displaymath}
   (L',i') \mapsto L'.
 \end{displaymath}
@@ -181,7 +181,7 @@ \section{Intermediate extensions and subgroups}
   K \defequi (Xg)^{\mkgroup B} \jdeq \prod_{x:B}X(g(x))
 \end{displaymath}
 It is a set, which can be equipped with a field structure, defined pointwise.
-Morevover, if one denotes $b$ for the distinguished point of $B$, and $(L'',j'')$ for $g(b)$, then, because $g$ is pointed, one has a path $p:L=L''$ such that $pi'=j''$. There are
+Moreover, if one denotes $b$ for the distinguished point of $B$, and $(L'',j'')$ for $g(b)$, then, because $g$ is pointed, one has a path $p:L=L''$ such that $pi'=j''$. There are
 fields extensions $i':k \to K$ and $j':K \to L$ given by:
 \begin{displaymath}
   i'(a) \defequi x\mapsto \snd(g(x))(a),\quad
@@ -189,7 +189,7 @@ \section{Intermediate extensions and subgroups}
 \end{displaymath}
 In particular, for all $a:k$, $j'i'(a) = \inv p \snd(g(b))(a) = \inv p j''(a) = i'(a)$.
 
-Galois theory is interested in the settings when these two contructions are inverse from each other.
+Galois theory is interested in the settings when these two constructions are inverse from each other.
 
 \section{separable/normal/etc.}
 \label{sec:cover-spac-fields-1}
diff --git a/geometry.tex b/geometry.tex
index 89804e0..88f153e 100644
--- a/geometry.tex
+++ b/geometry.tex
@@ -272,7 +272,7 @@ \section{Geometric objects}
 \begin{definition}
   Given an type $I$ and a family of geometric objects $T_i$ parametrized
   by the elements of $I$, an {\em arrangement} of the objects is a
-  configuration, also parametrized by the elements of $I$, whose $i$-th consituent is merely equal to
+  configuration, also parametrized by the elements of $I$, whose $i$-th constituent is merely equal to
   $T_i$.
 \end{definition}
 
diff --git a/group.tex b/group.tex
index 99966df..433a5c9 100644
--- a/group.tex
+++ b/group.tex
@@ -2826,7 +2826,7 @@ \subsection{Center of a group}
 There is a natural map
 $\ev_{\shape_G} : (\BG_\div\eqto\BG_\div) \to \BG_\div$ defined by
 $\ev_{\shape_G}(\varphi)\defequi \varphi(\shape_G)$, where the path
-$\varphi$ is coerced to a funciton through univalence. In particular,
+$\varphi$ is coerced to a function through univalence. In particular,
 $\ev_{\shape_G}(\refl{\BG_\div}) \jdeq \shape_G$. It makes the
 restriction of this map to the connected component of
 $\refl{\BG_\div}$ a pointed map. In other words, it defines a group
@@ -3067,7 +3067,7 @@ \subsection{Universal cover and simple connectedness}
 $\trp[\setTrunc{a\eqto\blank}]p$ is equal to the function
 $\alpha\mapsto \settrunc{p}\cdot \alpha$. In particular, there exists an
 equivalence from the type of path between two points $(x,\alpha)$ and
-$(y,\beta)$ of the universal cover $\univcover A a$ to sum type, analagous to
+$(y,\beta)$ of the universal cover $\univcover A a$ to sum type, analogous to
 the identification of paths in sum types:
 \begin{equation}
   \label{eq:id-types-universal-cover}%
@@ -3117,7 +3117,7 @@ \subsection{Universal cover and simple connectedness}
   determined by $\varphi_x \circ \settrunc\blank : a \eqto x \to \inv f (x)$. By induction on $p : a \eqto x$, we prove that
   $\varphi_x (\settrunc p) = \trp [\inv f] p (b , f_0) $ where $b$ is the element pointing $B$ and $f_0$ the path pointing $f$. Indeed, for
   $p \jdeq \refl a$, we get $\varphi_a (\settrunc {\refl a}) \jdeq (\varphi (\settrunc {\refl a}) , q_{\settrunc {\refl a}}) = (b , f_0)$
-  because $q$ is an indentification $\fst \eqto f \varphi$ of pointed functions.
+  because $q$ is an identification $\fst \eqto f \varphi$ of pointed functions.
 \end{proof}
 
 \subsection{Abelian groups and simply connected $2$-types}