Traditionally in dependent type theory with axiom K or uniqueness of identity proofs, every type $A$ is 0-truncated, and thus the type of lists on $A$, $\mathrm{List}(A)$, is 0-truncated and the free monoid on $A$. However, in homotopy type theory, not every type is 0-truncated; for example, the circle type $\mathbb{S}^1$ is a 1-truncated type which is provably not 0-truncated, and in general, types represent infinity-groupoids rather than sets. Thus, it makes sense to speak of the type of lists on the circle type, $\mathrm{List}(\mathbb{S}^1)$, or the type of lists on an arbitrary untruncated type $B$, $\mathrm{List}(B)$. Since neither $\mathbb{S}^1$ nor $B$ are provably 0-truncated, one cannot prove that the type of lists on $\mathbb{S}^1$ or $B$ is a monoid. However, in higher algebra, there is a structure which generalizes monoids from sets to infinity-groupoids, called $A\_\infty$-spaces. So is the list of types on $B$, $\mathrm{List}(B)$, the free $A\_\infty$-space on $B$?



Are lists in homotopy type theory free $A_\infty$-spaces?
In an informal sense, the answer "should be yes", in the sense that if one ignore type theory and work with an $\infty$-topos one can make sense of the construction $List(A)$ either by the usual universal property of list objects or as $List(A) = \coprod\_\mathbb{N} A^n$ (both definitions can be shown to be equivalent) and $List(A)$ is indeed the free $A\_\infty$-algebra on $A$.


However, the big problem is that we don't even know how to phrase the precise question you are asking in terms of Homotopy type theory, and it is not possible to make sense of what I just said (at least at the present time) within homotopy type theory. The problem is that we do not know how to define what is an $A\_\infty$-algebra within homotopy type theory. Being able to talk about this type of higher algebraic structure in HoTT, or show that it is impossible in some precise sense, is one of the biggest open problem in HoTT.


There are extensions of HoTT (like cubical HoTT, or maybe the simplicial HoTT of Riehl and Shulman with some additional work) that can/should be able to talk about higher structures like $A\_\infty$-algebras, and where this problem might have a solution, but I don't think it has been worked out in details.


The best one might hope to do in standard "book HoTT" (at least with present technology) is for each **external** (that is metatheoretical) integer $n$, define what is an $n$-truncated $A\_\infty$-algebra and show that for an $n$-truncated type, $List(A)$ is the free $n$-truncated $A\_\infty$-algebra on the type $A$. I even suspect we would only know how to do this for small values of $n$, though I might be wrong.


