# Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

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?

• Martin-Löf type theory proves that $A + B$ and $B + A$ are isomorphic types, so your solution for giving the monoid structure to a sum can't work. – Andrej Bauer Mar 7 '19 at 13:27
• Are you asking whether Martin-Löf type theory has an intepretation in the category of abelian monoids and monoid homomorphisms? – Andrej Bauer Mar 7 '19 at 13:28
• It is not clear what you are asking. Since the syntax of Martin-Löf type theory has only countably many types, but there is a proper class of non-isomorphic (abelian) monoids, the question in your title obviously has a negative answer, as stated. Furthermore, even if you say something like "I am only interested in finite monoids", you still have to explain how homomorphisms of monoids and monoid constructions are supposed to interact with type theory. Otherwise, I can just assign arbitrary monoid structures to the finite types, while making sure that I've covered all isomoprhism classes. – Andrej Bauer Mar 7 '19 at 14:21
• And then, at the end of the day, the answer will still be negative, because the category of abelian monoids has a zero object (the trivial monoid is both initial and terminal) but in type theory the empty and the unit type are distinct. – Andrej Bauer Mar 7 '19 at 14:24
• I don't see how that's necessary nor sufficient to make threadJoin useful. 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 to threadJoin that $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.) – Derek Elkins left SE Mar 8 '19 at 6:48

• The empty type does have a commutative binary operation, just with no identity. My rule for $A+B$ would actually only require $B$ to satisfy that weaker condition. I don't need every type to have the structure of an abelian monoid, just for enough of them to that any abelian monoid is isomorphic to some type (sans infinities concerns). – Andrew Cann Mar 9 '19 at 2:08