Monoidal.idr

Proposition

$\mathcal{C}ont$ is Monoidal in $⊳$ with unit $I$ proposition The sequencing product forms a monoidal structure in $\mathcal{C}ont$.

SequenceMonoidal : Monoidal Cont
SequenceMonoidal = MkMonoidal
    SequenceBifunctor
    I
    alpha
    leftUnitor
    rightUnitor