\[ \newcommand{\blank}{{-}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\nil}{\mathsf{nil}} \newcommand{\cons}{\mathsf{cons}} \newcommand{\iter}[2]{\mathsf{it}(#1, #2)} \newcommand{\id}{\mathsf{id}} \]
Let \(\cat{C}(1, \otimes)\) be a strict monoidal category, and \(A\) be an object of \(\cat{C}\).
A list algebra on \(A\) is an object \(L\) with a pair of maps \((1 \xrightarrow{n} L \xleftarrow{c} A \otimes L)\).
A list object on \(A\) is a list algebra \((1 \xrightarrow{\nil} L(A) \xleftarrow{\cons} A \otimes L(A))\), such that:
- for any \(P\)-parameterised list algebra \((P \xrightarrow{n} L \xleftarrow{c} A \otimes L)\), there is a unique map \(\iter{n}{c} : L(A) \otimes P \to L\) satisfying:
A monoid object \(M\) in \(\cat{C}\) is a pair of maps \((1 \xrightarrow{\epsilon} M \xleftarrow{\mu} M \otimes M)\) satisfying:
Lemma 1 \((1 \xrightarrow{\nil} L(A) \xleftarrow{\iter{\id}{\cons}} L(A))\) is a monoid structure on \(L(A)\).
Theorem 1 The list object construction gives \(L \dashv U : \mathsf{Mon}(\cat{C}) \to \cat{C}\).
Now, we switch to \(\cat{C}\) being symmetric strict monoidal, with symmetry \(\beta\).
A symmetric list object on \(A\) is a list object \((1 \xrightarrow{\nil} L(A) \xleftarrow{\cons} A \otimes L(A))\) satisfying:
Lemma 2 \((1 \xrightarrow{\nil} L(A) \xleftarrow{\iter{\id}{\cons}} L(A))\) is a commutative monoid structure on \(L(A)\).
Lemma 3 If \(L(A)\) is a list object on \(A\), the following are equivalent:
- \(L(A)\) is a symmetric list object on \(A\).
- \((L(A), \nil, \iter{\id}{\cons})\) is a commutative monoid.
- \((L(A), \nil, \iter{\id}{\cons}, \eta_A)\) is the free commutative monoid on \(A\).
Theorem 2 The symmetric list object construction gives \(L \dashv U : \mathsf{CMon}(\cat{C}) \to \cat{C}\).
Lemma 4 If \(\cat{C}\) is symmetric monoidal closed and has the relevant colimits, the following are equivalent:
- \(L(A)\) is a symmetric list object on \(A\).
- \(L(A)\) is the sequential colimit of the symmetric powers of \(A\).