(Free/Semifree) Multiplication on sigma types.

Stream: Is there code for X?

[Wrenna Robson]

Here's a notion.

Suppose I have β : ℕ → Type u such that I have an instance HMul (β n) (β n) (β (n + 1)) for all n. Consider Sigma β. I could define a free semigroup on this with FreeSemiGroup (Sigma β). Is it possible to define "the free semigroup on Sigma β, respecting the HMul on the β n" - i.e. if I have (n, a) and (n, b) in Sigma β, then in this "semi-free semigroup" their product will be (n + 1, a*b), but if I also have (m, c), then (n, a)*(m, c)*(n, b) won't interact unless m = n.

[Wrenna Robson]

This feels like a reasonably natural definition but if it exists I can't find it - is there a better way to do things like this?

[Wrenna Robson]

Effectively I want to lift the set of hetrogenous multiplications on the β n into one (associative) multiplication on Sigma β.

[Eric Wieser]

What do you mean by "won't interact"?

[Wrenna Robson]

As in a free multiplication, (n, a)*(m, c)*(n, b) simply "has no meaning" outside of what it is.

[Wrenna Robson]

It "doesn't cancel down" (I appreciate this language is imprecise).

[Eric Wieser]

Ah, but crucially you also mean "still type-checks"!

[Wrenna Robson]

Ah, yes, sorry - indeed!

[Wrenna Robson]

It's still a member of the type.

[Wrenna Robson]

Member? Do we say member for type? It typechecks, yes.

[Wrenna Robson]

I suppose ultimately this is a quotient by a suitable relation.

[Wrenna Robson]

Or something of that kind. I want (n, a)*(n, b) ~ (n + 1, a*b) and suchlike.

[Eric Wieser]

docs#Monoid.CoprodI looks somewhat related, though obviously doesn't use HMul

[Wrenna Robson]

No, nothing really seems to use HMul.

[Wrenna Robson]

Not sure about the transitivity of this relation.