Updates from Overleaf

papers/icfp24/code.sty

@@ -7,12 +7,12 @@
 % code listings
 \lstloadlanguages{Haskell}
 \lstdefinelanguage{Agda}{
-  aboveskip        = 0pt,
-  belowskip        = -1\baselineskip,
+  aboveskip        = \baselineskip,
+  belowskip        = \baselineskip,
   language         = Haskell,
   showstringspaces = false,
-  xleftmargin      = .01\textwidth,
-  xrightmargin     = .01\textwidth,
+  xleftmargin      = \parindent,
+  xrightmargin     = \parindent,
   columns          = fullflexible,
   keepspaces       = true,
   basewidth        = {0em,0em},
@@ -37,6 +37,7 @@
                      {->cm}{{\ensuremath{\xrightarrow{CMon}}}}2
                      {lambda}{{\ensuremath{\lambda\!}}}2
                      {forall}{{\ensuremath{\forall}}}2
+                     {Sg}{{\ensuremath{\Sigma}}}2
                      {times}{{\ensuremath{\times}}}2 {plus}{{+}}2 {uplus}{{\ensuremath{\uplus}}}2
                      {mem}{{\ensuremath{\in}}}2
                      {top}{{\ensuremath{\top}}}2 {bot}{{\ensuremath{\bot}}}2

papers/icfp24/free-commutative-monoids.tex

@@ -10,12 +10,14 @@ \subsection{Swap-List}
 
 \begin{code}
 data SList (A : UU) : UU where
-  [] : SList A
-  _::_ : A -> SList A -> SList A
+  nil : SList A
+  _cons_ : A -> SList A -> SList A
   swap : forall x y xs -> x :: y :: xs == y :: x :: xs 
   trunc : forall x y -> (p q : x == y) -> p == q
 \end{code}
 
+\vc{Explain trunc, why SList does but List doesn't? They both form endofunctors on $\Set$.}
+
 \subsection{Free monoid quotiented with permutation}
 We give a general construction of free commutative monoid as a free monoid quotient.
 Specific instances of this construction are given in \ref{cmon:plist} and \ref{cmon:bag}.

papers/icfp24/free-monoids.tex

@@ -9,13 +9,11 @@ \subsection{List}
 
 \begin{definition}{Lists}
 The type of lists on a type $A$ is given by:
-\vspace{1em}
 \begin{code}
 data List (A : UU) : UU where
   nil : List A
   _cons_ : A -> List A -> List A
 \end{code}
-\vspace{1em}
 \end{definition}
 
 An example of a list would be $3 :: 1 :: 2 :: []$, alternatively denoted as $[3, 1, 2]$ for convenience.
@@ -116,7 +114,7 @@ \subsection{Array}
 
 \begin{definition}{Arrays}
 The types of arrays on a type $A$ and $\Fin[n]$ are given by:
-\vspace{1em}
+\vc{These are weird notations.}
 \begin{code}
 Fin : $\mathbb{N}$ -> UU
 Fin n = $\Sigma$[ m $\in$ $\mathbb{N}$ ] (m < n)

papers/icfp24/introduction.tex

@@ -87,10 +87,16 @@ \subsection*{Solving the puzzle}
 This is a perfectly valid formalization of an ordered list! Empty lists and singleton lists
 are ordered, and we can inductively construct an "orderness witness" by prepending a new element
 to an ordered list, provided that the new element is less than the head of the old ordered list of
-course. This definition, however, assumes an existing total order on $A$. This is
+course. 
+
+A correct sort function then has the type: \inline{sort : List A -> Sg(xs:List A).Sorted xs}.\vc{How is ours better?}
+This definition, however, assumes an existing total order on $A$. This is
 unsatisfactory, in a way, because a sorting algorithm is fundamentally just a function. Can we
 axiomatize the correctness of a sorting algorithm purely by the properties of functions?
 
+\vc{Can you sort anything that doesn't have a total order?}
+\vc{Can you sort binary trees?}
+
 In a sense, this problem has already been solved, first by Hinze et al. \cite{10.1145/2364394.2364405}
 and later extended by Alexandru in their thesis \cite{alexandru_intrinsically_2023}.
 Their formalization is defined in terms of bialgebras, which not