Monoidal.idr

Proposition

$\mathcal{C}on{t}^{\#}$ is monoidal wrt the tensor on containers.

public export
ContCartMonoidal : Monoidal ContCart
ContCartMonoidal = MkMonoidal
    TensorBifunctorCart
    I
    alpha
    leftUnitor
    rightUnitor