For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be interpreted as abelian monoids. For the sum type $A + B$, you can define the monoid operation as: $$inj_L(a_0) \cdot inj_L(a_1) = inj_L(a_0 \cdot a_1)$$ $$inj_L(a) \cdot inj_R(b) = inj_R(b)$$ $$inj_R(b) \cdot inj_L(a) = inj_R(b)$$ $$inj_R(b_0) \cdot inj_R(b_1) = inj_R(b_0 \cdot b_1)$$ (Although this does mean that the interpretations of $A+B$ and $B+A$ are different).
So far though this scheme only lets me represent finite monoids where $\forall x: G, x \cdot x = x$. I'd like a way to extend it to infinite and more interesting monoids. That will at least require a way to interpret W-types but I can't see what that interpretation could be. Does such an interpretation exist? Or is there a simple proof that what I'm trying to do is impossible?