prose: fix typos

src/Cat/Displayed/TwoSided.lagda.md

@@ -46,12 +46,12 @@ A displayed category $\cE \liesover \cA \times \cB$ is a **two-sided fibration**
 when it satisfies the following 3 conditions:
 
 1. For every $u : \cA(A_1, A_2)$, $B : \cB$ and $Y : \cE_{A_2, B}$, there
-exists a [[cartesian lift]] $u^{*} : \cE_{u, \id}(u^{*}(Y), Y)$.
+exists a [[cartesian lift]] $\pi_{u, Y} : \cE_{u, \id}(u^{*}(Y), Y)$.
 
 2. For every $A : \cA, v : \cB(B_1, B_2)$ and $X : \cE_{A, B_1}$, there
-exists a [[cocartesian lift]] $v_{!} : \cE_{\id, v}(X, v_{!}(X))$.
+exists a [[cocartesian lift]] $\iota_{v, X} : \cE_{\id, v}(X, v_{!}(X))$.
 
-3. For every a diagram of the form below with $f$ cocartesian and $g$ cartesian,
+3. For every diagram of the form below with $f$ cocartesian and $g$ cartesian,
 $h$ is cartesian if and only if $k$ is cocartesian.
 
 ~~~{.quiver}
@@ -119,7 +119,7 @@ This definition is rather opaque, so let's break it down. The first two
 conditions ensure that we have 2 functorial actions on each of the [[fibre categories]]
 $E_{a, b}$: the first acts contravariantly in $\cA$, the second covariantly
 in $\cB$. This is analogous to the actions $P(-, \id)$ and $P(\id, -)$ for
-a profunctor $P : \cA \times \cB \to \Sets$. The final condition servers to
+a profunctor $P : \cA \times \cB \to \Sets$. The final condition serves to
 ensure that the [[base change]] and [[cobase change]] functors
-$u^{*} : \cE_{A_2, B} \to \cE_{A_1, B}$ and $v_{!} : \cE_{A, B_1} \to \cE{A, B_2}$
+$u^{*} : \cE_{A_2, B} \to \cE_{A_1, B}$ and $v_{!} : \cE_{A, B_1} \to \cE_{A, B_2}$
 preserve cocartesian and cartesian morphisms, resp.

src/Cat/Displayed/TwoSided/Discrete.lagda.md

@@ -291,7 +291,7 @@ $u : \cA(A_1, A_2), v : \cB(B_1, B_2)$.
 
 All of our Hom sets are propositional, so constructing an inverse only
 requires us to build a map $\cE_{u^{-1}, v^{-1}}(Y, X)$. Moreover, it
-suffices to prove that $(u^{-1})^{*}(X) = v^{-1}_{!}(X)$, which follows
+suffices to prove that $(u^{-1})^{*}(X) = (v^{-1})_{!}(X)$, which follows
 from some tedious functoriality algebra.
 
 ```agda