0
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Mar 7 at 13:27
  • $\begingroup$ Are you asking whether Martin-Löf type theory has an intepretation in the category of abelian monoids and monoid homomorphisms? $\endgroup$ – Andrej Bauer Mar 7 at 13:28
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Mar 7 at 14:21
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Mar 7 at 14:24
  • 1
    $\begingroup$ 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.) $\endgroup$ – Derek Elkins Mar 8 at 6:48
0
$\begingroup$

Fortunately you gave us some context in the comments (always a good idea to include it in your question). Rather than doing what you're trying to do, I believe quantitative type theory is what you're looking for.

$\endgroup$
  • $\begingroup$ QTT is my starting point. I'm basically trying to turn it into a process calculus with an in-built notion of commutativity. $\endgroup$ – Andrew Cann Mar 8 at 7:41
  • $\begingroup$ Do you want every type to have an intrinsic structure of an abelian monoid? The empty type might pose a problem, what will its unit be? $\endgroup$ – Andrej Bauer Mar 8 at 10:52
  • $\begingroup$ 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). $\endgroup$ – Andrew Cann Mar 9 at 2:08
  • $\begingroup$ Ugh, I totally missed the word "some" in the title. Maybe emphasize that bit a little more. $\endgroup$ – Andrej Bauer Mar 9 at 9:11
  • $\begingroup$ Sorry, I'm guessing my using the words "interpret" and "represented" led to confusion by making it sound like I was talking about model theory or something (?). Also it wasn't really a good question since it's far too specific to my niche problem. Thanks though. $\endgroup$ – Andrew Cann Mar 11 at 5:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.