more minor cleanups

papers/icfp24/combinatorics.tex

@@ -143,7 +143,10 @@ \subsection{Other combinatorial properties}
 %
 However, more often than not, they both do not exhibit the same properties, for example:
 \begin{itemize}
-    \item The coproduct of two (free) commutative monoids is given by their underlying cartesian product
+    \item
+        Generally, $\FF(A + B)$ is the coproduct of $\FF(A)$ and $\FF(B)$.
+        For (free) commutative monoids, this is equivalent to
+        their underlying cartesian product
           (dual of Fox's theorem~\cite{foxCoalgebrasCartesianCategories1976}),
           that is, $\MM(A + B) \eqv \MM(A) \times \MM(B)$.
           %

papers/icfp24/free-commutative-monoids.tex

@@ -391,7 +391,9 @@ \subsection{Bag}\label{cmon:bag}
 
 It suffices to show that $\ext{f}$ is invariant under permutation: for all $\phi\colon \Fin[n]\xto{\sim}\Fin[n]$,
 $\ext{f}(n, i) \id \ext{f}(n, i \circ \phi)$. To prove this we first need to develop some formal combinatorics of
-\emph{punching in} and \emph{punching out} indices. These operations are developed further
+\emph{punching in} and \emph{punching out} indices. These operations are
+borrowed from~\cite{mozlerCubicalAgdaSimple2021} and
+developed further
 in~\cite{choudhurySymmetriesReversibleProgramming2022} for studying permutation codes.
 
 \begin{lemma}\label{bag:tau}

papers/icfp24/universal-algebra.tex

@@ -235,7 +235,8 @@ \subsection{Free Algebras}
     \label{prop:free-algebra-colimits}
     \leavevmode
     \begin{itemize}
-        \item $\str{F}(\emptyt) \eqv \unitt$, is a zero object in $\sigAlg$,
+        \item $\sigAlg(\str{F}(\emptyt), \str{X}) \eqv \unitt$, 
+        \item there is a unique algebra map $\str{F}(\unitt) \to \unitt$,
         \item $\str{F}(X + Y)$ is the coproduct of $\str{F}(X)$ and $\str{F}(Y)$ in $\sigAlg$:
               \[
                   \sigAlg(\str{F}(X + Y), \str{Z}) \eqv
@@ -511,6 +512,11 @@ \subsection{Equations}
 The construction of the free object in this variety requires non-constructive principles~\cite[Section 7, pg 142]{blassWordsFreeAlgebras1983},
 in particular, the arity sets need to be projective, so we do not give the general construction.
 %
-Of course, HITs are another way to write higher generators for equations~\cite{univalentfoundationsprogramHomotopyTypeTheory2013}.
+The non-constructive principles can be avoided if we limit ourselves to specific constructions
+where everything is finitary.
+%
+Of course, HoTT offers an alternative to non-constructive principles by allowing us
+write higher generators for equations with HITs
+~\cite{univalentfoundationsprogramHomotopyTypeTheory2013}.
 %
 We do not develop the framework further, and instead consider the specific cases of constructions of free monoids and free commutative monoids in the next sections.