done with 3.7?

circle.tex

@@ -2445,7 +2445,7 @@ \section{Interlude: combinatorics of permutations}
 The two groups of parentheses indicate the two cycles,
 and the order within a group indicates the cyclic order.
 Since the starting point in a cycle doesn't matter,
-we could also have written $(3\;1\;2)(5\;4)$.
+we could also have written, \eg $(3\;1\;2)(5\;4)$.
 
 In general, if $a_1,a_2,\dots,a_k$ are pairwise distinct elements of a decidable set $A$,
 then we write $(a_1\;a_2\;\cdots\;a_k)$ for the permutation of $A$
@@ -2469,6 +2469,10 @@ \section{Interlude: combinatorics of permutations}
 
   It's only for decidable $X$, however, that we can express these
   cycles as cyclic permutations.
+  \MB{Alternative: Note that cyclic permutations can move at most finitely many elements,
+  and cannot give, \eg the infinite cycle $(\zet,\zs)$. 
+  Moreover, to define the cycle $(X,t)$ from, 
+  \eg the transposition $(x\;x')$ requires that the set $X$ is decidable.}
 \end{remark}
 
 \begin{definition}\label{def:support-permutation}
@@ -2496,14 +2500,15 @@ \section{Interlude: combinatorics of permutations}
   \]
 \end{xca}
 \begin{corollary}
-  Any permutation of a finite set can be expressed a composition of transpositions.
+  Any permutation of a finite set can be expressed as
+  a composition of transpositions.
 \end{corollary}
 To show this, first write the permutation as a composition of cyclic permutations,
 then apply~\cref{xca:perm-prod-transpositions} to each cycle.\footnote{%
   This representation is not unique, as for example $(1\;2)=(2\;3)(1\;3)(2\;3)$
   as permutations of $\set{1,2,3}$.
-  Below, in~\cref{cor:sign-defined}, we'll show that the \emph{parity} (odd/even)
-  of the number of transitions is invariant, however.}
+  However, in~\cref{cor:sign-defined} below, we'll show that 
+  the \emph{parity} (odd/even) of the number of transitions is invariant.}
 
 \begin{xca}
   Show that there are $n!$ permutations of a finite set of cardinality $n$, where $n! \defeq \fact(n)$ is the usual notation for the factorial function.
@@ -2521,7 +2526,7 @@ \section{Interlude: combinatorics of permutations}
     $\Aut(X \coprod \bn 1) \equivto (X \coprod \bn 1)' \times \Aut(X)$,
     where
     \[
-      Y' \defeq \sum_{y : Y}\prod_{z : Y}(y \eqto z \coprod y \ne z).
+      Y' \defeq \sum_{y : Y}\prod_{z : Y}((y \eqto z) \coprod ((y \eqto z)\to\emptytype).
     \]
     By a local version of Hedberg's~\cref{thm:hedberg},
     $Y'$ is a subtype of $Y$.}%