Merge overleaf-2024-02-27-1127 into main

papers/icfp24/combinatorics.tex

@@ -123,9 +123,10 @@ \subsection{Seely isomorphism}
 \end{equation*}
 
 \cite{choudhuryFreeCommutativeMonoids2023} have given a proof on this property. We give a diagram here
-showing how this equivlance can be constructed.
+showing how this equivalence can be constructed.
 
-\begin{center}
+\begin{figure}[H]
+    \centering
 % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXE1NKEEpXFx0aW1lc1xcTU0oQikiXSxbMSwxLCJcXE1NKEErQikgXFx0aW1lcyBcXE1NKEErQikiXSxbMiwwLCJcXE1NKEEgKyBCKSJdLFswLDEsIlxcTU0oaV8xKSBcXHRpbWVzIFxcTU0oaV8yKSIsMix7ImxhYmVsX3Bvc2l0aW9uIjowfV0sWzEsMiwiXFxvdGltZXNfeyhBK0IpfSIsMix7ImxhYmVsX3Bvc2l0aW9uIjoxMDB9XSxbMCwyLCJcXHNpbWVxIl1d
 \begin{tikzcd}[ampersand replacement=\&,cramped]
 	{\MM(A)\times\MM(B)} \&\& {\MM(A + B)} \\
@@ -134,7 +135,9 @@ \subsection{Seely isomorphism}
 	\arrow["{\otimes_{(A+B)}}"'{pos=1}, from=2-2, to=1-3]
 	\arrow["\simeq", from=1-1, to=1-3]
 \end{tikzcd}
-\end{center}
+    \caption{Construction of the Seely isomorphism}
+    \label{fig:enter-label}
+\end{figure}
 
 This property does not hold for free monoids, because $\LL(A + B)$ is larger than $\LL(A) \times \LL(B)$.
 Given $a: A$ and $b: B$, we can only construct $([a], [b]) : \LL(A) \times \LL(B)$, however we can
@@ -165,4 +168,19 @@ \subsection{Path space}
 \redtext{Say something about Path space. Cons is injective.}
 
 \subsection{Head}
-
+Consider the $\term{head} : \FF(A) \to A$ function which takes an element out of $\FF(A)$.
+We consider by cases on the length of $\FF(A)$.
+
+Case 0: $\term{head}$ cannot be defined, for example if $A = \emptyt$, such a function would lead to
+a contradiction.
+
+Case 1: $\term{head}$ can be defined for both $\MM(A)$ and $\LL(A)$. In fact, it is a equivalence
+if we only consider $xs : \FF(A)$ where $\term{length}(xs) = 1$, with its inverse given by $\eta_A$.
+
+Case $n \geq 2$: $\term{head}$ can be defined for any $\LL(A)$. Using $\List$ as an example, one can simply
+take the first element of the list. However, for $\MM(A)$, $\term{head}$ can only be defined if it
+respects commutativity. Using $\SList$ as an example, this means $\term{head}$ must satisfy:
+$\term{head}(x :: y :: xs) = \term{head}(y :: x :: xs)$ for any $x, y : A$ and $xs : \SList(A)$.
+This implies if we were to define $\term{head}$ for $\MM(A)$, we must be able to order or sort a
+list $xs$ of $A$ somehow, so we can pick a "least" or "biggest" element $x \in xs$ such that for any
+permutation of $xs$ $xs^*$, $\term{head}(xs^*) = x$.

papers/icfp24/free-commutative-monoids.tex

@@ -2,7 +2,6 @@ \section{Construction of Free Commutative Monoids}
 \label{sec:commutative-monoids}
 
 We now extend our constructions of free monoids to free commutative monoids.
-\vc{Discuss what's good and what's bad about each presentation.}
 
 \subsection{Free monoid quotiented with permutation}\label{cmon:qfreemon}
 We give a general construction of free commutative monoid as a free monoid quotient.

papers/icfp24/free-monoids.tex

@@ -126,7 +126,6 @@ \subsection{Array}
 
 \begin{definition}{Arrays}\label{mon:array}
 The types of $\Array$ on a type $A$ and $\Fin[n]$ are given by:
-\vc{These are weird notations.}
 \begin{code}
 Fin : $\mathbb{N}$ -> UU
 Fin n = $\Sigma$[ m $\in$ $\mathbb{N}$ ] (m < n)

papers/icfp24/macros.sty

@@ -47,9 +47,6 @@
 % ++
 \newcommand\doubleplus{\mathbin{\text{\ttfamily\upshape ++}}}
 
-% Unit
-\newcommand{\unitt}{{\mathbf{1}}}
-
 % Bool
 \newcommand{\boolt}{{\mathbf{2}}}
 

papers/icfp24/sorting.tex

@@ -4,6 +4,24 @@ \section{Sorting}
 \vc{This theorem works for any presentation.}
 \vc{Different presentations can be advantageous to different kinds of sorting algorithms.}
 
+Consider the canonical map $q : \LL(A) \to \MM(A)$ given by $\ext{\eta_A}$. $q$ would be a surjective
+function which "forgets" the order on a free monoid and turns it into a free commutative monoid.
+The axiom of choice says every surjection $f$ has a section $s$ such that $\forall x.\, f(s(x)) = x$.
+
+\begin{figure}[H]
+    \centering
+    \scalebox{1.3}{
+        % https://q.uiver.app/#q=WzAsMixbMCwwLCJcXExMKEEpIl0sWzMsMCwiXFxNTShBKSJdLFsxLDAsInMiLDAseyJjdXJ2ZSI6LTF9XSxbMCwxLCJxIiwwLHsiY3VydmUiOi0xfV1d
+    \begin{tikzcd}[ampersand replacement=\&,cramped]
+    	{\LL(A)} \&\&\& {\MM(A)}
+    	\arrow["s", curve={height=-6pt}, from=1-4, to=1-1]
+    	\arrow["q", curve={height=-6pt}, two heads, from=1-1, to=1-4]
+    \end{tikzcd}
+    }
+    \caption{Relationship of $\LL(A)$ and $\MM(A)$}
+    \label{fig:enter-label}
+\end{figure}
+
 We can now study sort functions as sections and their relationship with total orders.
 First, we recall the axioms of total order are:
 \begin{itemize}