Change definition of smash

[Alizter]

I think a better definition of Smash would be as the cofiber of the wedge inclusion map. This might make it less busy of a definition. Currently we have all these auxiliary points and different path constructors which make it confusing to reason about.

[jdchristensen]

This is equivalent to having point constructors sm : X * Y -> Smash X Y and aux : Smash X Y, path constructors sm x pt = aux and sm pt y = aux, and a 2-path constructor saying that the two paths sm pt pt = aux are equal. Because of the 2-cell, I'm worried that we'd end up with 3- or 4-cells when dealing with homotopies. But maybe there's a way to avoid that somehow? And maybe it would let us combine symmetrical arguments? Not sure how, since we'd need to case split on the wedge, I think.

This approach is what Axel Ljungström used very successfully in https://arxiv.org/abs/2402.03523, but I think what made his approach successful was other insights, not this particular choice of model for the smash product.

[Alizter]

It seems to be more technologically advantageous to have lower dimensional constructors even if the arguments get longer. I will therefore close this discussion as I don't see any immediate advantage over what we currently have. Lots of little easy pieces is still easier than a few very hard ones.