Tags: Unit of the normalization monad, Multiplication of the normalization monad, produoidal normalization.