free product of 2 groups

Stream: Is there code for X?

[Yury G. Kudryashov]

Am I right that we have a free product of an indexed family of groups but we don't have a free product of 2 groups? If that's correct, then I'm going to fix this. Also, I'm going to add @[to_additive] here and there. What names would you suggest? I need 4 names (additive/multiplicative * indexed family/two types).

[Yury G. Kudryashov]

I want to formalize this because the groups $\mathbb Z_2*(\mathbb Z_2\times\mathbb Z_2)$ and $(\mathbb Z_2\times\mathbb Z_2)*(\mathbb Z_2\times\mathbb Z_2)$ are useful pre-quotients for formalizing theorems/doing computations about Grigorchuk group.

[David Wärn]

I think that's correct. You could take indexed families over bool but it will need some API

[Adam Topaz]

Using indexed families over bool will introduce unnecessary universe restrictions

[Adam Topaz]

Presumably you want the free product $G \star H$ to be in universe max v u when G : Type v and H : Type u.

[David Wärn]

Ah yes. You could get around it by first lifting G and H to Type (max v u) and then forming the family over bool. But I don't know if it's easier than writing a new construction

[Yury G. Kudryashov]

I already have a construction in branch#YK-grigorchuk file data/ncword that works in both settings (and we can redo free groups using this construction too). I wonder how should I call these objects.

[Yury G. Kudryashov]

About a family indexed by bool. It would be nice to have a tactic that specializes some constructions from pi types to products and from sigma types to sums using families indexed by boolean indexes and ulift. But this indeed needs some work.