Merge overleaf-2024-03-01-0803 into main

papers/icfp24/free-commutative-monoids.tex

@@ -107,9 +107,9 @@ \subsection{Free monoids with a quotient}\label{cmon:qfreemon}
     for any commutative monoid homomorphism $f : {F(A) / \approx} \to \mathfrak{X}$ and $x : {F(A) / \approx}$,
     $\ext{(f \comp \eta_A)}(x) = f(x)$. To prove this it is suffice to show for all $x : F(A)$,
     $\ext{(f \comp \eta_A)}(q(x)) = f(q(x))$.
-    $\ext{(f \comp \eta_A)}(q(x))$ reduces to $\widehat{(f \comp q \comp \mu_A)}(x)$.
+    $\ext{(f \comp \eta_A)}(q(x))$ reduces to $\exthat{(f \comp q \comp \mu_A)}(x)$.
     Note that both $f$ and $q$ are homomorphism, therefore $f \comp q$ is a homomorphism. By
-    universal property of $F$ we get $\widehat{(f \comp q \comp \mu_A)}(x) = (f \comp q)(x)$,
+    universal property of $F$ we get $\exthat{(f \comp q \comp \mu_A)}(x) = (f \comp q)(x)$,
     therefore $\ext{(f \comp \eta_A)}(q(x)) = f(q(x))$.
 
     We have now shown that $(\blank) \comp \eta_A$ is an equivalence from

papers/icfp24/math.sty

@@ -36,7 +36,7 @@
 \newcommand{\str}[1]{\mathfrak{#1}}
 
 \newcommand{\ext}[1]{{#1}^{\sharp}}
-\newcommand{\exthat}[1]{{#1}^{\bar{\sharp}}}
+\newcommand{\exthat}[1]{\widehat{#1}}
 
 \newcommand{\eq}{\term{eq}}
 \newcommand{\fv}{\term{fv}}