diff --git a/categories.tex b/categories.tex
index 567c397a..28d5400f 100644
--- a/categories.tex
+++ b/categories.tex
@@ -339,7 +339,7 @@ \section{Functors and transformations}
 \end{lem}
 \begin{proof}
   If $\gamma$ is an isomorphism, then we have $\delta:G\to F$ that is its inverse.
-  By definition of composition in $B^A$, $(\delta\gamma)_a\jdeq \delta_a\gamma_a$ and similarly.
+  By definition of composition in $B^A$, $(\delta\gamma)_a\jdeq \delta_a\gamma_a$ and similarly $(\gamma\delta)_a\jdeq \gamma_a\delta_a$.
   Thus, $\id{\delta\gamma}{1_F}$ and $\id{\gamma\delta}{1_G}$ imply $\id{\delta_a\gamma_a}{1_{Fa}}$ and $\id{\gamma_a\delta_a}{1_{Ga}}$, so $\gamma_a$ is an isomorphism.
 
   Conversely, suppose each $\gamma_a$ is an isomorphism, with inverse called $\delta_a$, say.
@@ -453,7 +453,7 @@ \section{Functors and transformations}
   \cref{ct:functor-assoc} is coherent, i.e.\ the following pentagon\index{pentagon, Mac Lane} of equalities commutes:
   \[ \xymatrix{ & K(H(GF)) \ar@{=}[dl] \ar@{=}[dr]\\
     (KH)(GF) \ar@{=}[d] && K((HG)F) \ar@{=}[d]\\
-    ((KH)G)F && (K(HG))F \ar@{=}[ll] }
+    ((KH)G)F && (K(HG))F \ar@{=}[ll].}
   \]
 \end{lem}
 \begin{proof}
@@ -464,7 +464,7 @@ \section{Functors and transformations}
 We have a similar coherence result for units.
 
 \begin{lem}\label{ct:units}
-  For a functor $F:A\to B$, we have equalities $\id{(1_B\circ F)}{F}$ and $\id{(F\circ 1_A)}{F}$, such that given also $G:B\to C$, the following triangle of equalities commutes.
+  For a functor $F:A\to B$, we have equalities $\id{(1_B\circ F)}{F}$ and $\id{(F\circ 1_A)}{F}$, such that given also $G:B\to C$, the following triangle of equalities commutes:
   \[ \xymatrix{
     G\circ (1_B \circ F) \ar@{=}[rr] \ar@{=}[dr] &&
     (G\circ 1_B)\circ F \ar@{=}[dl] \\
@@ -551,7 +551,7 @@ \section{Equivalences}
   \indexdef{precategory!equivalence of}%
   \index{functor!equivalence}%
   if it is a left adjoint for which $\eta$ and $\epsilon$ are isomorphisms.
-  We write $\cteqv A B$ for the type of equivalences of categories from $A$ to $B$.
+  We write $\cteqv A B$ for the type of equivalences of (pre)categories from $A$ to $B$.
 \end{defn}
 
 By \cref{ct:adjprop,ct:isoprop}, if $A$ is a category, then the type ``$F$ is an equivalence of precategories'' is a mere proposition.