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?
threadJoinuseful. Either $T$ is fixed, in which case you can either prove or assert that it has the structure of a (commutative) monoid, or $T$ is arbitrary, in which case the most natural thing would be to pass in a proof tothreadJointhat $T$ is a monoid. A third alternative is $T$ is arbitrary, but we restrict the introduction rules of $?$ to only allow types with a monoid structure. None of this requires every monoid to be "representable" as a type in some manner. (Also, I'd suspect users would care which monoid gets used.) $\endgroup$