Monoid.idr

List Monoids

Proposition

The $ListCont$ container is a monoid wrt to cartesian product $(\ast )$ in $\mathcal{C}ont$

ListMonoidCartesian : MonoidObject {o = Container} {cat = Cont} CartesianMonoidal

This statement is equivalent to saying that $Lista\in \mathcal{S}et$ is a monoid with the empty list as neutral element and concatenation as multiplication.

Proposition

The $ListCont$ container is a monoid wrt composition $(⊳)$ in $\mathcal{C}on{t}^{\#}$

  ListMonoid : MonoidObject {o = Container} {cat = ContCart} SequenceMonoidal

• finish diagrams conditions

This statement is equivalent to saying that $List\in \mathcal{S}et\to \mathcal{S}et$ is a monad in $\mathcal{C}on{t}^{\#}$.